BetweennessMiddleTransitivity Show Code edit
thm (BetweennessMiddleTransitivity () () (→ (∧ (between A B D) (between B C D)) (between A C D))
B C A D BetweennessMiddleTransitivityBEqualsC
(→ (= B C) (→ (∧ (between A B D) (between B C D)) (between A C D)))
B C A D BetweennessMiddleTransitivityBNotEqualC
(→ (¬ (= B C)) (→ (∧ (between A B D) (between B C D)) (between A C D)))
eliminateCases
(→ (∧ (between A B D) (between B C D)) (between A C D))
)
edit