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

end;

( between a,t,s implies x = y )

proof

assume between a,t,s ; :: thesis: 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; :: thesis: verum

end;

hence x = y by A4, A1, A2, A3, Satz5p2; :: thesis: verum