let S be satisfying_Tarski-model TarskiGeometryStruct ; for a, b, c, r, x, y being POINT of S st r <> a & b <> c & a out x,r & a,x equiv b,c & a out y,r & a,y equiv b,c holds
x = y
let a, b, c, r, x, y be POINT of S; ( r <> a & b <> c & a out x,r & a,x equiv b,c & a out y,r & a,y equiv b,c implies x = y )
assume A1:
( r <> a & b <> c & a out x,r & a,x equiv b,c & a out y,r & a,y equiv b,c )
; x = y
consider s being POINT of S such that
A2:
( s <> a & between x,a,s & between r,a,s )
by A1, Satz6p3;
consider t being POINT of S such that
A3:
( t <> a & between y,a,t & between r,a,t )
by A1, Satz6p3;
A4:
( between a,s,t implies x = y )
proof
assume
between a,
s,
t
;
x = y
then
(
between x,
s,
t &
between x,
a,
t )
by A2, Satz3p7p1, Satz3p7p2;
then
(
between t,
a,
x &
between t,
a,
y )
by A3, Satz3p2;
hence
x = y
by A1, A3, Satz2p12;
verum
end;
( between a,t,s implies x = y )
proof
assume
between a,
t,
s
;
x = y
then
(
between y,
t,
s &
between y,
a,
s )
by A3, Satz3p7p1, Satz3p7p2;
then
(
between s,
a,
y &
between s,
a,
x )
by A2, Satz3p2;
hence
x = y
by A1, A2, Satz2p12;
verum
end;
hence
x = y
by A4, A1, A2, A3, Satz5p2; verum