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

(→ (∧ (∧ (∧ (∧ (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) (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))

)