is_image := fun P' P A B => (exists X, is_midpoint X P P' /\ Col A B X) /\ (Perp A B P P' \/ P = P')
forall A B P P1 P2, A ≠ B → is_image P1 P A B → is_image P2 P A B → P1 = P2
forall A B P, exists P', is_image P' P A B
forall A B P P', is_image P P' A B → is_image P' P A B
forall A B P P' P'', A ≠ B → is_image P' P A B → is_image P'' P' A B → P = P''
forall A B P P1 P2, A ≠ B → is_image P P1 A B → is_image P P2 A B → P1 = P2
forall A B P', A ≠ B → exists P, is_image P' P A B
forall A B P P' Q Q', A ≠ B → is_image P' P A B → is_image Q' Q A B → P'= Q' → P = Q
forall A B P, A ≠ B → is_image P P A B → Col P A B
forall A B P Q P' Q', A<>B → is_image P' P A B → is_image Q' Q A B → Cong P Q P' Q'
forall A B C A' B' C', Per A B C → Per A' B' C' → Cong A B A' B' → Cong B C B' C' → Cong A C A' C'