let S be non empty satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for x, y, z, a, b, c, c9, p, q, q9 being POINT of S st not Collinear a,b,c & between b,a,y & a <> y & between a,y,z & y,z equiv y,p & y <> p & q9 = reflection (z,q) & Middle c,x,c9 & c <> y & between q9,y,c9 & Middle y,p,c & between p,y,q & q <> q9 holds
x <> y
let x, y, z, a, b, c, c9, p, q, q9 be POINT of S; :: thesis: ( not Collinear a,b,c & between b,a,y & a <> y & between a,y,z & y,z equiv y,p & y <> p & q9 = reflection (z,q) & Middle c,x,c9 & c <> y & between q9,y,c9 & Middle y,p,c & between p,y,q & q <> q9 implies x <> y )
assume that
A1: not Collinear a,b,c and
A2: between b,a,y and
A3: a <> y and
A4: between a,y,z and
A5: y,z equiv y,p and
A6: y <> p and
A7: q9 = reflection (z,q) and
A8: Middle c,x,c9 and
A9: c <> y and
A10: between q9,y,c9 and
A11: Middle y,p,c and
A12: between p,y,q and
A13: q <> q9 ; :: thesis: x <> y
assume A14: x = y ; :: thesis: contradiction

now :: thesis: ( y in Line (a,b) & a <> y & a <> b )

Collinear b,a,y by A2, GTARSKI1:def 17;
hence y in Line (a,b) by LemmaA1; :: thesis: ( a <> y & a <> b )
thus a <> y by A3; :: thesis: a <> b
thus a <> b by A1, GTARSKI3:46; :: thesis: verum

end;

then A15: Line (a,y) = Line (a,b) by GTARSKI3:82;

now :: thesis: ( z in Line (y,a) & y <> a & y <> z )

Collinear a,y,z by A4, GTARSKI1:def 17;
hence z in Line (y,a) by LemmaA1; :: thesis: ( y <> a & y <> z )
thus y <> a by A3; :: thesis: y <> z
thus y <> z by A5, A6, GTARSKI1:def 7, GTARSKI3:4; :: thesis: verum

end;

then A16: Line (y,z) = Line (a,b) by A15, GTARSKI3:82;
A17: Line (x,c) = Line (x,c9) by A8, A9, A14, Prelim10;
Collinear x,c9,q9 by A10, A14, GTARSKI1:def 17;
then A18: q9 in Line (x,c) by A17, LemmaA1;
( between c,p,x & between p,x,q & p <> x ) by A14, A6, A11, A12, GTARSKI3:def 12, GTARSKI3:14;
then between c,x,q by GTARSKI3:19;
then Collinear c,x,q by GTARSKI1:def 17;
then q in Line (c,x) by LemmaA1;
then A19: Line (q,q9) = Line (c,x) by A13, A9, A14, A18, Prelim11;
Middle q,z,q9 by A7, GTARSKI3:def 13;
then between q,z,q9 by GTARSKI3:def 12;
then Collinear q,z,q9 by GTARSKI1:def 17;
then Collinear q,q9,z by GTARSKI3:45;
then z in Line (c,x) by A19, LemmaA1;
then Collinear z,c,x by LemmaA2;
then Collinear y,z,c by A14, GTARSKI3:45;
then c in Line (a,b) by A16, LemmaA1;
then Collinear c,a,b by LemmaA2;
hence contradiction by A1, GTARSKI3:45; :: thesis: verum