le := fun A B C D => exists y, Bet C y D /\ Cong A B C y
ge := fun A B C D => le C D A B
forall A B C D : Point, A ≠ B → Bet A B C → Bet A B D → Bet A C D \/ Bet A D C
forall A B C D : Point, A ≠ B → Bet A B C → Bet A B D → Bet B C D \/ Bet B D C
forall A B C D : Point, Bet A B D → Bet A C D → Bet A B C \/ Bet A C B
forall A B C D : Point, le A B C D → exists x, Bet A B x /\ Cong A x C D
forall A B C D, (exists x, Bet A B x /\ Cong A x C D) → le A B C D
forall A B C D A' B' C' D', le A B C D /\ Cong A B A' B' /\ Cong C D C' D' → le A' B' C' D'
forall A B, le A B A B
forall A B C D E F, le A B C D → le C D E F → le A B E F
forall A B C, Bet A C B → Cong A C A B → C=B
forall A B D E, Bet A D B → Bet A E B → Cong A D A E → D = E
forall A B C D, le A B C D → le C D A B → Cong A B C D
forall A Q B C, A ≠ Q → exists X, (Bet Q A X \/ Bet Q X A) /\ Cong Q X B C
forall A C D, le A A C D
forall A B C D : Point, le A B C D \/ le C D A B
forall A B C, le A B C C → A = B
lt := fun A B C D => le A B C D /\ ~ Cong A B C D
gt := fun A B C D => lt C D A B.