theorem Lemma5p12p2: :: GTARSKI3:67

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d being POINT of S st a,b <= c,d holds
a,b <= d,c