List of theorems in general/Out_lines.gh:

(↔ (is-outside P A B) (∧ (∧ (¬ (= A P)) (¬ (= B P))) (∨ (between P A B) (between P B A))))

(→ (∧ (∧ (∧ (∧ (¬ (= A P)) (¬ (= B P))) (¬ (= C P))) (between A P C)) (between B P C)) (is-outside P A B))

(→ (∧ (∧ (∧ (∧ (¬ (= A P)) (¬ (= B P))) (¬ (= C P))) (between A P C)) (is-outside P A B)) (∨ (∧ (∧ (¬ (= A P)) (between A P C)) (between P A B)) (∧ (∧ (¬ (= A P)) (between A P C)) (between P B A))))

(→ (∧ (∧ (∧ (∧ (¬ (= A P)) (¬ (= B P))) (¬ (= C P))) (between A P C)) (is-outside P A B)) (between B P C))

(→ (∧ (∧ (∧ (¬ (= A P)) (¬ (= B P))) (¬ (= C P))) (between A P C)) (↔ (between B P C) (is-outside P A B)))

(→ (∧ (is-outside P A B) (∧ (¬ (= C P)) (between A P C))) (between B P C))

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

(→ (is-outside P A B) (∃ c (∧ (∧ (¬ (= c P)) (between A P c)) (between B P c))))

(→ (is-outside P A B) (∧ (∧ (¬ (= A P)) (¬ (= B P))) (∃ c (∧ (∧ (¬ (= c P)) (between A P c)) (between B P c)))))

(→ (∧ (∧ (¬ (= A P)) (¬ (= B P))) (∃ c (∧ (∧ (¬ (= c P)) (between A P c)) (between B P c)))) (is-outside P A B))

(↔ (is-outside P A B) (∧ (∧ (¬ (= A P)) (¬ (= B P))) (∃ c (∧ (∧ (¬ (= c P)) (between A P c)) (between B P c)))))

(→ (∧ (∧ (¬ (= A P)) (¬ (= B P))) (between P A B)) (¬ (between A P B)))

(→ (∧ (∧ (¬ (= A P)) (¬ (= B P))) (between P B A)) (¬ (between A P B)))

(→ (is-outside P A B) (¬ (between A P B)))

(→ (is-outside P A B) (collinear A P B))

(→ (is-outside P A B) (∧ (collinear A P B) (¬ (between A P B))))

(→ (∧ (collinear A P B) (¬ (between A P B))) (∧ (¬ (= A P)) (¬ (= B P))))

(→ (∧ (collinear A P B) (¬ (between A P B))) (∨ (between P A B) (between P B A)))

(→ (∧ (collinear A P B) (¬ (between A P B))) (is-outside P A B))

(↔ (is-outside P A B) (∧ (collinear A P B) (¬ (between A P B))))

(→ (¬ (= A P)) (is-outside P A A))

(↔ (is-outside P A B) (is-outside P B A))

(→ (∧ (¬ (= B P)) (∧ (∨ (between P A B) (between P B A)) (∨ (between P B C) (between P C B)))) (∨ (between P A C) (between P C A)))

(→ (∧ (is-outside P A B) (is-outside P B C)) (is-outside P A C))

(→ (∧ (∧ (¬ (= R A)) (¬ (= B C))) (∧ (∨ (between A R E) (between A E R)) (≡ A E B C))) (∧ (is-outside A E R) (≡ A E B C)))

(→ (∧ (¬ (= R A)) (¬ (= B C))) (∃ e (∧ (is-outside A e R) (≡ A e B C))))

(→ (∧ (∧ (∧ (∧ (∧ (¬ (= R A)) (¬ (= B C))) (is-outside A X R)) (≡ A X B C)) (is-outside A Y R)) (≡ A Y B C)) (∨ (∨ (∧ (between A X R) (between A Y R)) (∧ (between A X R) (between A R Y))) (∨ (∧ (between A R X) (between A Y R)) (∧ (∧ (¬ (= A R)) (between A R X)) (between A R Y)))))

(→ (∧ (∧ (∧ (∧ (∧ (¬ (= R A)) (¬ (= B C))) (is-outside A X R)) (≡ A X B C)) (is-outside A Y R)) (≡ A Y B C)) (∨ (between A X Y) (between A Y X)))

(→ (∧ (∧ (∧ (∧ (∧ (¬ (= R A)) (¬ (= B C))) (is-outside A X R)) (≡ A X B C)) (is-outside A Y R)) (≡ A Y B C)) (≡ A X A Y))

(→ (∧ (∧ (∧ (∧ (∧ (¬ (= R A)) (¬ (= B C))) (is-outside A X R)) (≡ A X B C)) (is-outside A Y R)) (≡ A Y B C)) (= X Y))

(→ (∧ (is-outside P A B) (≤ P A P B)) (∃ y (∧ (is-outside P A B) (∧ (between P y B) (≡ P A P y)))))

(→ (∧ (is-outside P A B) (∧ (between P Y B) (≡ P A P Y))) (¬ (= P Y)))

(→ (∧ (is-outside P A B) (∧ (between P Y B) (≡ P A P Y))) (is-outside P Y B))

(→ (∧ (is-outside P A B) (∧ (between P Y B) (≡ P A P Y))) (= Y A))

(→ (∧ (is-outside P A B) (∧ (between P Y B) (≡ P A P Y))) (between P A B))

(→ (∧ (is-outside P A B) (≤ P A P B)) (between P A B))

(→ (between P A B) (≤ P A P B))

(→ (is-outside P A B) (↔ (≤ P A P B) (between P A B)))

(→ (∨ (between P S X) (between P X S)) (collinear X P S))

(→ (∧ (∧ (¬ (= P Q)) (collinear S P Q)) (collinear X P Q)) (collinear X P S))

(→ (∧ (∧ (¬ (= P Q)) (collinear P Q A)) (collinear P Q B)) (collinear P A B))

(→ (∧ (∧ (∧ (¬ (= P Q)) (¬ (= S P))) (collinear S P Q)) (collinear X P Q)) (collinear X P S))

(→ (∧ (∧ (∧ (¬ (= P Q)) (¬ (= S P))) (collinear S P Q)) (collinear X P S)) (collinear X P Q))

(→ (∧ (∧ (¬ (= P Q)) (¬ (= S P))) (collinear S P Q)) (↔ (collinear X P Q) (collinear X P S)))

(→ (∧ (∧ (¬ (= P Q)) (collinear P Q A)) (collinear P Q B)) (collinear Q A B))

(→ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= C D))) (collinear A B P)) (collinear A B Q)) (collinear C D P)) (collinear C D Q)) (collinear C P Q))

(→ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= C D))) (collinear A B P)) (collinear A B Q)) (collinear C D P)) (collinear C D Q)) (¬ (= A B)))

(→ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= C D))) (collinear A B P)) (collinear A B Q)) (collinear C D P)) (collinear C D Q)) (∧ (∧ (¬ (= A B)) (collinear A B P)) (collinear A B Q)))

(→ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= C D))) (collinear A B P)) (collinear A B Q)) (collinear C D P)) (collinear C D Q)) (collinear A P Q))

(→ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= C D))) (collinear A B P)) (collinear A B Q)) (collinear C D P)) (collinear C D Q)) (collinear B P Q))

(→ (∧ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= C D))) (collinear A B P)) (collinear A B Q)) (collinear C D P)) (collinear C D Q)) (¬ (= P Q))) (collinear P Q A))

(→ (∧ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= C D))) (collinear A B P)) (collinear A B Q)) (collinear C D P)) (collinear C D Q)) (¬ (= P Q))) (collinear P Q C))

(→ (∧ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= C D))) (collinear A B P)) (collinear A B Q)) (collinear C D P)) (collinear C D Q)) (¬ (= P Q))) (collinear A C Q))

(→ (∧ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= C D))) (collinear A B P)) (collinear A B Q)) (collinear C D P)) (collinear C D Q)) (¬ (= P Q))) (collinear P Q B))

(→ (∧ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= C D))) (collinear A B P)) (collinear A B Q)) (collinear C D P)) (collinear C D Q)) (¬ (= P Q))) (collinear A B Q))

(→ (∧ (= Q A) (∧ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= C D))) (collinear A B P)) (collinear A B Q)) (collinear C D P)) (collinear C D Q)) (¬ (= P Q)))) (collinear A B C))

(→ (∧ (¬ (= Q A)) (∧ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= C D))) (collinear A B P)) (collinear A B Q)) (collinear C D P)) (collinear C D Q)) (¬ (= P Q)))) (collinear A B C))

(→ (∧ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= C D))) (collinear A B P)) (collinear A B Q)) (collinear C D P)) (collinear C D Q)) (¬ (= P Q))) (collinear A B C))

(→ (∧ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= C D))) (collinear A B P)) (collinear A B Q)) (collinear C D P)) (collinear C D Q)) (¬ (= P Q))) (⊥))

(→ (∧ (∧ (∧ (∧ (∧ (¬ (collinear A B C)) (¬ (= C D))) (collinear A B P)) (collinear A B Q)) (collinear C D P)) (collinear C D Q)) (= P Q))

(∃ a (∃ b (∃ c (¬ (collinear a b c)))))

(→ (¬ (collinear A B P)) (∃ c (¬ (collinear A B c))))

(→ (∧ (= A X) (∧ (∧ (collinear A B X) (∧ (collinear A B Y) (¬ (= A B)))) (collinear A B Z))) (collinear X Y Z))

(→ (∧ (¬ (= A X)) (∧ (∧ (collinear A B X) (∧ (collinear A B Y) (¬ (= A B)))) (collinear A B Z))) (collinear X Y Z))

(→ (∧ (∧ (collinear A B X) (∧ (collinear A B Y) (¬ (= A B)))) (¬ (collinear X Y Z))) (¬ (collinear A B Z)))

(→ (∧ (∧ (collinear A B Y) (¬ (= A B))) (¬ (collinear X Y Z))) (∃ c (¬ (collinear A B c))))

(→ (∧ (¬ (= A B)) (¬ (collinear X Y Z))) (∃ c (¬ (collinear A B c))))

(→ (¬ (= A B)) (∃ c (¬ (collinear A B c))))

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

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

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

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