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 IFS a9,b9,c9,d9 holds
b,d equiv b9,d9
let a, b, c, d, a9, b9, c9, d9 be POINT of S; :: thesis: ( a,b,c,d IFS a9,b9,c9,d9 implies b,d equiv b9,d9 )
assume A1: a,b,c,d IFS a9,b9,c9,d9 ; :: thesis: b,d equiv b9,d9
per cases ( a = c or a <> c ) ;
suppose A2: a = c ; :: thesis: b,d equiv b9,d9
now :: thesis: ( c = b & c9 = b9 )
thus c = b by A1, A2, GTARSKI1:def 10; :: thesis: c9 = b9
a9 = c9 by A1, A2, Satz2p2, GTARSKI1:def 7;
hence c9 = b9 by A1, GTARSKI1:def 10; :: thesis: verum
end;
hence b,d equiv b9,d9 by A1; :: thesis: verum
end;
suppose A3: a <> c ; :: thesis: b,d equiv b9,d9
consider e being POINT of S such that
A4: ( between a,c,e & c,e equiv a,c ) by GTARSKI1:def 8;
A5: c <> e by A3, A4, Satz2p2, GTARSKI1:def 7;
consider e9 being POINT of S such that
A6: ( between a9,c9,e9 & c9,e9 equiv c,e ) by GTARSKI1:def 8;
A7: c,e equiv c9,e9 by A6, Satz2p2;
S is satisfying_SST_A5 ;
then A8: e,d equiv e9,d9 by A3, A4, A6, A1, A7;
c,b equiv b9,c9 by A1, Satz2p4;
then A9: c,b equiv c9,b9 by Satz2p5;
e9,c9 equiv c,e by A6, Satz2p4;
then e9,c9 equiv e,c by Satz2p5;
then A17: e,c equiv e9,c9 by Satz2p2;
A18: between e,c,b
proof
( between b,c,e & between a,b,e ) by A1, A4, Satz3p6p1, Satz3p6p2;
hence between e,c,b by Satz3p2; :: thesis: verum
end;
A19: between e9,c9,b9
proof
( between b9,c9,e9 & between a9,b9,e9 ) by A1, A6, Satz3p6p1, Satz3p6p2;
hence between e9,c9,b9 by Satz3p2; :: thesis: verum
end;
S is satisfying_SST_A5 ;
hence b,d equiv b9,d9 by A19, A18, A8, A9, A17, A1, A5; :: thesis: verum
end;
end;