List of theorems

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))
(→ antecedent (between A B C))(→ antecedent (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)))