IndivisibilityBiconditional Show Code edit
thm (IndivisibilityBiconditional () () (↔ (between x y x) (= x y))
x y Indivisibility
(→ (between x y x) (= x y))
x x BetweenAAB
(between x x x)
x EqualityReflexivity
(= x x)
x EqualityReflexivity
(= x x)
x x x y x x BetweenBuilder
(→ (∧ (∧ (= x x) (= x y)) (= x x)) (↔ (between x x x) (between x y x)))
detach2of2
(→ (∧ (= x x) (= x y)) (↔ (between x x x) (between x y x)))
detach1of2
(→ (= x y) (↔ (between x x x) (between x y x)))
detachImplicationBiconditional
(→ (= x y) (between x y x))
introduceBiconditionalFromImplications
(↔ (between x y x) (= x y))
)
edit