fact: Definition alternative_proclus_postulate := forall A B C D P Q, Perp2 A B C D P -> ~ Col C D P -> Coplanar A B C D -> Col A B P -> ~ Col A B Q -> Coplanar C D P Q -> exists Y, Col P Q Y /\ Col C D Y.
imports: GeoCoq.Tarski_dev.Definitions