let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: 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
let a, b, c, d, e, f, g, h be Element of S; :: thesis: ( not c,d <= a,b & a,b equiv e,f & c,d equiv g,h implies e,f <= g,h )
( a,b <= c,d or c,d <= a,b ) by Satz5p10;
hence ( not c,d <= a,b & a,b equiv e,f & c,d equiv g,h implies e,f <= g,h ) by Satz5p6; :: thesis: verum