let S be satisfying_Tarski-model TarskiGeometryStruct ; for a, b, c, p being POINT of S ex x being POINT of S st
( ( between p,a,x or between p,x,a ) & p,x equiv b,c )
let a, b, c, p be POINT of S; ex x being POINT of S st
( ( between p,a,x or between p,x,a ) & p,x equiv b,c )
set q = p;
consider r being POINT of S such that
A1:
( between a,p,r & p,r equiv a,p )
by GTARSKI1:def 8;
consider x being POINT of S such that
A2:
( between r,p,x & p,x equiv b,c )
by GTARSKI1:def 8;
A3:
( r = p implies ( ( between p,a,x or between p,x,a ) & p,x equiv b,c ) )
by A1, A2, Satz2p2, GTARSKI1:def 7;
( r <> p implies ( ( between p,a,x or between p,x,a ) & p,x equiv b,c ) )
proof
assume A4:
r <> p
;
( ( between p,a,x or between p,x,a ) & p,x equiv b,c )
between r,
p,
a
by A1, Satz3p2;
hence
( (
between p,
a,
x or
between p,
x,
a ) &
p,
x equiv b,
c )
by A2, A4, Satz5p2;
verum
end;
hence
ex x being POINT of S st
( ( between p,a,x or between p,x,a ) & p,x equiv b,c )
by A3; verum