fact: Definition strong_parallel_postulate := forall P Q R S T U, BetS P T Q -> BetS R T S -> ~ Col P R U -> Coplanar P Q R U -> Cong P T Q T -> Cong R T S T -> exists I, Col S Q I /\ Col P U I.
imports: GeoCoq.Tarski_dev.Definitions