BetweennessEquality Show Code edit
thm (BetweennessEquality ( ) () (→ (∧ (between A B C) (between B A C)) (= A B))
A B C B A a Pasch
(→ (∧ (between A B C) (between B A C)) (∃ a (∧ (between B a B) (between A a A))))
# That gives us <code>∃ a (between B a B ∧ between A a A)</code>. We just need to apply the <code>BetweenSubstitution</code> lemma to get <code>between A B A</code>,
a B A A BetweenSubstitution
(→ (∃ a (∧ (between B a B) (between A a A))) (between A B A))
applySyllogism
(→ (∧ (between A B C) (between B A C)) (between A B A))
# which in turn implies <code>A = B</code>
A B Indivisibility
(→ (between A B A) (= A B))
applySyllogism
(→ (∧ (between A B C) (between B A C)) (= A B))
)
edit