Per := fun A B C => exists C', is_midpoint B C C' /\ Cong A C A C'
forall A B C, Per A B C → Per C B A
forall A B C A', Per A B C → A ≠ B → Col B A A' → Per A' B C
forall A B C C', Per A B C → is_midpoint B C C' → Per A B C'
forall A B, Per A B B
forall A B C A', Per A B C → Per A' B C → Bet A C A' → B = C
forall A B C, Per A B C → Per A C B → B = C
forall A B, Per A B A → A = B
forall A B C, Per A B C → Col A B C → A = B \/ C = B
forall A B C A' B' C', Per A B C → Cong_3 A B C A' B' C' → Per A' B' C'
Perp_in := fun X A B C D =>
A ≠ B /\ C ≠D /\ Col X A B /\ Col X C D /\ (forall U V, Col U A B → Col V C D → Per U X V)
Perp := fun A B C D => exists X, Perp_in X A B C D
forall A B C D X, Perp_in X A B C D → Perp_in X C D A B
forall A B C D X,
A ≠ B → C ≠ D → Col X A B → Col X C D →
(exists U, exists V, Col U A B /\ Col V C D /\ U ≠ X /\ V ≠ X /\ Per U X V) → Perp_in X A B C D.
forall A B, ~ Perp A B A B
forall X A B C D, Perp_in X A B C D → Perp A B C D
forall X A B C D Y, Perp_in X A B C D → Col Y A B → Col Y C D → X=Y
forall A B C D X, Perp A B C D → Col X A B → Col X C D → Perp_in X A B C D
forall X A B C D, Perp A B C D → (forall Y, Col Y A B → Col Y C D → X = Y) → Perp_in X A B C D
forall A B C D X Y, Perp_in X A B C D → Perp_in Y A B C D → X = Y
forall A B C X, A ≠ B → Col A B X → Perp A B C X → Perp_in X A B C X
forall A B C X, A<>B → Col A B X → Perp_in X A B C X → Perp A B C X
forall A B C U X, A ≠ B → Col A B X → Col A B U → U<>X → Perp A B C X
→ ~ Col A B C /\ Per C X U
forall A B C U X,
A<>B → Col A B X → Col A B U → U<>X → ~ Col A B C → Per C X U → Perp A B C X
forall A B C X Y,
~ Col A B C → Col A B X → Perp A B C X → Col A B Y → Perp A B C Y → X = Y
forall A B C, ~ Col A B C → exists X, Col A B X /\ Perp A B C X
forall A B C C' D P,
Per A B C → is_midpoint P C' D → is_midpoint A C' C → is_midpoint B D C → Per B A P
forall A B C C' D P,
Per A B C → is_midpoint P C' D → is_midpoint A C' C → is_midpoint B D C → B ≠ C → A ≠ P
forall A B C, A ≠ B → exists P, exists T, Perp A B P A /\ Col A B T /\ Bet C T P
forall A B C D, Perp A B C D → Perp C D A B
forall A B C D, Perp A B C D → Perp B A D C
forall A B C D, Perp A B C D → Perp B A C D
forall A B C D, Perp A B C D → Perp A B D C
forall A B C D X, Perp_in X A B C D → Perp_in X B A C D
forall A B C D X, Perp_in X A B C D → Perp_in X A B D C
forall A B C D X, Perp_in X A B C D → Perp_in X B A D C
forall A B C D X, Perp_in X A B C D → Perp_in X C D A B
forall A B C, A<>B → Perp A B C A → Per B A C
forall A B C, A<>B → Perp A B A C → Per B A C
forall A B C D E, A ≠ E → Perp A B C D → Col A B E → Perp A E C D
forall A B C D, Perp A B C D → A ≠ B
forall A B C D, Perp A B C D → C ≠ D
forall A B C, Perp A B C A → Perp_in A A B C A
forall A B, exists X, is_midpoint X A B
forall A B P R X ,
A ≠ B → A ≠ P → Per B A P → Per A B R →
Cong A P B R → Bet A X B → Bet P X R →
Cong A R P B /\ is_midpoint X A B /\ is_midpoint X P R