BetweennessInnerTransitivityFlipped Show Code edit
thm (BetweennessInnerTransitivityFlipped () () (→ (∧ (between A B C) (between A C D)) (between B C D))
# We first rewrite <code>between A B C</code> into <code>between C B A</code> and <code>between A C D</code> into <code>between D C A</code>
A B C BetweennessSymmetry
(↔ (between A B C) (between C B A))
A C D BetweennessSymmetry
(↔ (between A C D) (between D C A))
buildConjunction
(↔ (∧ (between A B C) (between A C D)) (∧ (between C B A) (between D C A)))
eliminateBiconditionalReverse
(→ (∧ (between A B C) (between A C D)) (∧ (between C B A) (between D C A)))
# Now we switch the order of the conjuncts.
(between C B A) (between D C A) ConjunctionCommutativity
(↔ (∧ (between C B A) (between D C A)) (∧ (between D C A) (between C B A)))
eliminateBiconditionalReverse
(→ (∧ (between C B A) (between D C A)) (∧ (between D C A) (between C B A)))
applySyllogism
(→ (∧ (between A B C) (between A C D)) (∧ (between D C A) (between C B A)))
# Now we are ready to apply inner transitivity (which, when expanded with these variables, works out to <code>between D C A ∧ between C B A → between D C B</code>)
D C A B BetweennessInnerTransitivity
(→ (∧ (between D C A) (between C B A)) (between D C B))
applySyllogism
(→ (∧ (between A B C) (between A C D)) (between D C B))
# Turning <code>between D C B</code> into <code>between B C D</code> finishes the proof.
swapBetweennessInConsequent
(→ (∧ (between A B C) (between A C D)) (between B C D))
)
edit