BetweennessInnerTransitivity Show Code edit
thm (BetweennessInnerTransitivity ( ) ()
(→ (∧ (between A B D) (between B C D)) (between A B C))
A B D B C a Pasch
(→ (∧ (between A B D) (between B C D)) (∃ a (∧ (between B a B) (between C a A))))
# That gives us <code>∃ a (between B a B ∧ between C a A)</code>. The <code>BetweenSubstitution</code> lemma turns this into <code>between C B A</code>, and we just need to switch the order of the endpoints to be done.
a B C A BetweenSubstitution
(→ (∃ a (∧ (between B a B) (between C a A))) (between C B A))
applySyllogism
(→ (∧ (between A B D) (between B C D)) (between C B A))
swapBetweennessInConsequent
(→ (∧ (between A B D) (between B C D)) (between A B C))
)
edit