fact: Definition universal_posidonius_postulate := forall A1 A2 A3 A4 B1 B2 B3 B4, Par A1 A2 B1 B2 -> Col A1 A2 A3 -> Col B1 B2 B3 -> Perp A1 A2 A3 B3 -> Col A1 A2 A4 -> Col B1 B2 B4 -> Perp A1 A2 A4 B4 -> Cong A3 B3 A4 B4.
imports: GeoCoq.Tarski_dev.Definitions