let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: 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; :: thesis: 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 ; :: thesis: ( ( 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; :: thesis: 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; :: thesis: verum