two_sides := fun A B P Q => A<>B /\ ~ Col P A B /\ ~ Col Q A B /\ exists T, Col T A B /\ Bet P T Q
forall A B P Q, two_sides A B P Q → two_sides A B Q P
forall A B X Y M N,
Col A B M→ Col X Y M → Col A B N → Col X Y N →
~ Col A X B → X <> Y → M = N
forall P Q A C M R B,
two_sides P Q A C → Col M P Q → is_midpoint M A C → Col R P Q →
out R A B →
two_sides P Q B C
forall P Q A C R S M,
two_sides P Q A C
→ Col R P Q → Perp P Q A R
→ Col S P Q → Perp P Q C S
→ is_midpoint M R S → (forall U V, is_midpoint M U V → (out R U A ↔ out S C V))
forall P Q A C R S U V,
two_sides P Q A C
→ Col R P Q → Perp P Q A R
→ Col S P Q → Perp P Q C S
→ out R U A → out S V C → two_sides P Q U V
forall P Q A C R B, two_sides P Q A C → Col R P Q → out R A B → two_sides P Q B C
forall A B C P Q, Bet A C P → Bet B Q C → exists X, Bet A X B /\ Bet P Q X
one_side := fun P Q A B => exists C, two_sides P Q A C /\ two_sides P Q B C
forall P Q A B C, two_sides P Q A C → one_side P Q A B → two_sides P Q B C
forall P Q A B, two_sides P Q A B → ~ one_side P Q A B
forall P Q A B, one_side P Q A B → ~ two_sides P Q A B
forall P Q A, P ≠ Q → ~ Col A P Q → exists C, two_sides P Q A C
forall P Q A, ~ Col A P Q → one_side P Q A A
forall P Q A B, one_side P Q A B → one_side P Q B A
forall P Q A B C, one_side P Q A B → one_side P Q B C → one_side P Q A C