BetweennessBuilder Show Code edit
thm (BetweennessBuilder () () (
(∧ (∧ (= x0 y0) (= x1 y1)) (= x2 y2)) (↔ (between x0 x1 x2) (between y0 y1 y2))
)
x0 y0 x1 y1 x2 y2 BetweenBuilder
(→ (∧ (∧ (= x0 y0) (= x1 y1)) (= x2 y2)) (↔ (between x0 x1 x2) (between y0 y1 y2)))
)
edit