theorem Satz6p28Lem02: :: GTARSKI3:94

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d, e, f, g, h being Element of S st not c,d <= a,b & a,b equiv e,f & c,d equiv g,h holds
e,f <= g,h