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 FS a9,b9,c9,d9 & a <> b holds
c,d equiv c9,d9
let a, b, c, d, a9, b9, c9, d9 be POINT of S; :: thesis: ( a,b,c,d FS a9,b9,c9,d9 & a <> b implies c,d equiv c9,d9 )
assume A1: ( a,b,c,d FS a9,b9,c9,d9 & a <> b ) ; :: thesis: c,d equiv c9,d9
then Collinear a,b,c ;
per cases then ( between a,b,c or between b,c,a or between c,a,b ) ;
suppose A2: between a,b,c ; :: thesis: c,d equiv c9,d9
then A3: between a9,b9,c9 by A1, Satz4p6;
A4: ( a,b equiv a9,b9 & a,c equiv a9,c9 & b,c equiv b9,c9 ) by A1, GTARSKI1:def 3;
S is satisfying_SST_A5 ;
hence c,d equiv c9,d9 by A1, A4, A2, A3; :: thesis: verum
end;
suppose A5: between b,c,a ; :: thesis: c,d equiv c9,d9
b,c,a cong b9,c9,a9 by A1, Lm4p13p1;
then b,c,a,d IFS b9,c9,a9,d9 by A5, Satz4p6, A1;
hence c,d equiv c9,d9 by Satz4p2; :: thesis: verum
end;
suppose between c,a,b ; :: thesis: c,d equiv c9,d9
then A6: between b,a,c by Satz3p2;
A7: b,a,c cong b9,a9,c9 by A1, Lm4p14p1;
A8: between b9,a9,c9 by A6, A7, Satz4p6;
S is satisfying_SST_A5 ;
hence c,d equiv c9,d9 by A1, A8, A6, A7; :: thesis: verum
end;
end;