fact: Definition euclid_s_parallel_postulate := forall A B C D P Q R, OS B C A D -> SAMS A B C B C D -> SumA A B C B C D P Q R -> ~ Bet P Q R -> exists Y, Out B A Y /\ Out C D Y.
imports: GeoCoq.Tarski_dev.Definitions