BetweennessOuterTransitivityFlipped-sub Show Code edit
thm (BetweennessOuterTransitivityFlipped-sub () () (→ (∧ (= a D) (between A C a)) (between A C D))
A EqualityReflexivity
(= A A)
C EqualityReflexivity
(= C C)
A A C C a D BetweenBuilder
(→ (∧ (∧ (= A A) (= C C)) (= a D)) (↔ (between A C a) (between A C D)))
detach2of3
(→ (∧ (= A A) (= a D)) (↔ (between A C a) (between A C D)))
detach1of2
(→ (= a D) (↔ (between A C a) (between A C D)))
# That gives us <code>a = D → (between A C a ↔ between A C D)</code>.
eliminateBiconditionalReverseInConsequent
(→ (= a D) (→ (between A C a) (between A C D)))
import
(→ (∧ (= a D) (between A C a)) (between A C D))
)
edit