fact: Definition existential_playfair_s_postulate := exists A1 A2 P, ~ Col A1 A2 P /\ (forall B1 B2 C1 C2, Par A1 A2 B1 B2 -> Col P B1 B2 -> Par A1 A2 C1 C2 -> Col P C1 C2 -> Col C1 B1 B2 /\ Col C2 B1 B2).
imports: GeoCoq.Tarski_dev.Definitions