BetweennessOuterTransitivityFlipped Show Code edit
thm (BetweennessOuterTransitivityFlipped ( ) () (→ (∧ (∧ (between A B C) (between B C D)) (¬ (= B C))) (between A C D))
A B C D a BetweennessOuterTransitivityFlipped-2
(→ (∧ (∧ (between A B C) (between B C D)) (¬ (= B C))) (∃ a (∧ (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D)) (¬ (= B C)))))
A C a D B BetweennessOuterTransitivityFlipped-aca-ad
(→ (∧ (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D)) (¬ (= B C))) (∧ (= a D) (between A C a)))
a D A C BetweennessOuterTransitivityFlipped-sub
(→ (∧ (= a D) (between A C a)) (between A C D))
applySyllogism
(→ (∧ (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D)) (¬ (= B C))) (between A C D))
a addThereExists
(→ (∃ a (∧ (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D)) (¬ (= B C)))) (∃ a (between A C D)))
applySyllogism
(→ (∧ (∧ (between A B C) (between B C D)) (¬ (= B C))) (∃ a (between A C D)))
removeThereExistsInConsequent
(→ (∧ (∧ (between A B C) (between B C D)) (¬ (= B C))) (between A C D))
)
edit