fact: Definition bachmann_s_lotschnittaxiom := forall P Q R P1 R1, P <> Q -> Q <> R -> Per P Q R -> Per Q P P1 -> Per Q R R1 -> Coplanar P Q R P1 -> Coplanar P Q R R1 -> exists S, Col P P1 S /\ Col R R1 S.
imports: GeoCoq.Tarski_dev.Definitions