List of theorems in general/Betweenness_of_points.gh:

(between A B B)

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

(→ (between A B C) (between C B A))

(↔ (between A B C) (between C B A))

(between A A B)

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

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

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

(→ (∧ (∧ (between A C x) (≡ C x C D)) (between A B C)) (∧ (∧ (between A C x) (≡ C x C D)) (between B C x)))

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

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

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

(→ (∧ (= a D) (between A C a)) (between A C D))

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

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

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

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

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

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

(↔ (between x y x) (= x y))

IndivisibilityBidirectional deprecated synonym

(↔ (between x y x) (= x y))
(∃ a (∃ b (∃ c (∨ (¬ (= a b)) (¬ (= b c))))))

(↔ (∃ a (∃ b (¬ (= a b)))) (∃ b (∃ c (¬ (= b c)))))

(∃ a (∃ b (¬ (= a b))))

(→ (∧ (= A B) (≡ A B C D)) (= C D))

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

(→ (∧ (∧ (between A B C) (≡ B C x y)) (¬ (= x y))) (∧ (between A B C) (¬ (= B C))))

(∃ c (∧ (between A B c) (¬ (= B c))))

(∃ b (¬ (= A b)))

(→ (∧ (∧ (between A B C) (between A′ B′ C)) (between A P A′)) (∃ q (∧ (between P q C) (between B q B′))))

(→ (∧ (∧ (= x0 y0) (= x1 y1)) (= x2 y2)) (↔ (between x0 x1 x2) (between y0 y1 y2)))