let S be satisfying_Tarski-model TarskiGeometryStruct ; 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; ( 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 )
; 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
;
c,d equiv c9,d9then 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;
verum end; suppose A5:
between b,
c,
a
;
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;
verum end; suppose
between c,
a,
b
;
c,d equiv c9,d9then 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;
verum end; end;