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))

)