BetweennessOuterTransitivityFlipped-2
Show Code edit

thm (BetweennessOuterTransitivityFlipped-2 ((A a) (B a) (C a) (D a)) ()

(→

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

# First, <code>C a ≡ C D ∧ between B C a</code>.

A B C D a BetweennessOuterTransitivityFlipped-bca

(→ (∧ (∧ (between A B C) (between B C D)) (¬ (= B C))) (∃ a (∧ (∧ (between A C a) (≡ C a C D)) (between B C a))))

# Next, <code>between B C D</code>

(∧ (between A B C) (between B C D)) (¬ (= B C)) ConjunctionRightElimination

(→ (∧ (∧ (between A B C) (between B C D)) (¬ (= B C))) (∧ (between A B C) (between B C D)))

eliminateLeftConjunctInConsequent

(→ (∧ (∧ (between A B C) (between B C D)) (¬ (= B C))) (between B C D))

composeConjunction

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

a (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D) ThereExistsConjunctionRightMovement

(↔ (∃ a (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D))) (∧ (∃ a (∧ (∧ (between A C a) (≡ C a C D)) (between B C a))) (between B C D)))

eliminateBiconditionalForward

(→ (∧ (∃ a (∧ (∧ (between A C a) (≡ C a C D)) (between B C a))) (between B C D)) (∃ a (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D))))

applySyllogism

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

# Finally, <code>B ≠ C</code>

(∧ (between A B C) (between B C D)) (¬ (= B C)) ConjunctionLeftElimination

(→ (∧ (∧ (between A B C) (between B C D)) (¬ (= B C))) (¬ (= B C)))

composeConjunction

(→ (∧ (∧ (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 (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (between B C D)) (¬ (= B C)) ThereExistsConjunctionRightMovement

(↔ (∃ a (∧ (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (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))))

eliminateBiconditionalForward

(→ (∧ (∃ a (∧ (∧ (∧ (between A C a) (≡ C a C D)) (between B C a)) (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)))))

applySyllogism

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

)