let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c, d, a9, b9, c9, d9 being POINT of S st a,b <= c,d & a,b equiv a9,b9 & c,d equiv c9,d9 holds
a9,b9 <= c9,d9
let a, b, c, d, a9, b9, c9, d9 be POINT of S; :: thesis: ( a,b <= c,d & a,b equiv a9,b9 & c,d equiv c9,d9 implies a9,b9 <= c9,d9 )
assume A1: ( a,b <= c,d & a,b equiv a9,b9 & c,d equiv c9,d9 ) ; :: thesis: a9,b9 <= c9,d9
then consider x being POINT of S such that
A2: ( between a,b,x & a,x equiv c,d ) by Satz5p5;
Collinear a,b,x by A2;
then consider y being POINT of S such that
A3: a,b,x cong a9,b9,y by A1, Satz4p14;
a9,y equiv c9,d9
proof
a9,y equiv a,x by A3, Satz2p2;
then a9,y equiv c,d by A2, Satz2p3;
hence a9,y equiv c9,d9 by A1, Satz2p3; :: thesis: verum
end;
hence a9,b9 <= c9,d9 by A2, A3, Satz4p6, Satz5p5; :: thesis: verum