let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, p, q being POINT of S holds p,q equiv reflection (a,p), reflection (a,q)
let a, p, q be POINT of S; :: thesis: p,q equiv reflection (a,p), reflection (a,q)
reconsider p9 = reflection (a,p), q9 = reflection (a,q) as POINT of S ;

per cases ( p = a or p <> a ) ;

suppose A1: p = a ; :: thesis: p,q equiv reflection (a,p), reflection (a,q)

Middle q,a, reflection (a,q) by DEFR;
hence p,q equiv reflection (a,p), reflection (a,q) by A1, Satz7p10; :: thesis: verum

end;

suppose A2: p <> a ; :: thesis: p,q equiv reflection (a,p), reflection (a,q)

A3: Middle p,a,p9 by DEFR;
A4: Middle q,a,q9 by DEFR;
consider x being POINT of S such that
A5: between p9,p,x and
A6: p,x equiv q,a by GTARSKI1:def 8;
consider y being POINT of S such that
A7: between q9,q,y and
A8: q,y equiv p,a by GTARSKI1:def 8;
consider x9 being POINT of S such that
A9: between x,p9,x9 and
A10: p9,x9 equiv q,a by GTARSKI1:def 8;
consider y9 being POINT of S such that
A11: between y,q9,y9 and
A12: q9,y9 equiv p,a by GTARSKI1:def 8;
A13: ( between5 x,p,a,p9,x9 & between5 y,q,a,q9,y9 )

proof

A14: between x9,p9,x by A9, Satz3p2;
between p9,a,p by A3, Satz3p2;
then between5 x9,p9,a,p,x by A5, A14, Satz3p11p3pb, Satz3p11p4pb;
hence between5 x,p,a,p9,x9 by Satz3p2; :: thesis: between5 y,q,a,q9,y9
A15: between y9,q9,y by A11, Satz3p2;
between q9,a,q by A4, Satz3p2;
then between5 y9,q9,a,q,y by A7, A15, Satz3p11p3pb, Satz3p11p4pb;
hence between5 y,q,a,q9,y9 by Satz3p2; :: thesis: verum

end;

A16: a,x equiv a,y

proof

A17: p,a equiv q,y by A8, Satz2p2;
x,p equiv q,a by A6, Satz2p4;
then A18: x,p equiv a,q by Satz2p5;
( between x,p,a & between a,q,y ) by A13, Satz3p2;
then x,a equiv a,y by A17, A18, Satz2p11;
hence a,x equiv a,y by Satz2p4; :: thesis: verum

end;

A19: a,y equiv a,x9

proof

q,a equiv p9,x9 by A10, Satz2p2;
then a,q equiv p9,x9 by Satz2p4;
then A20: a,q equiv x9,p9 by Satz2p5;
q,y equiv a,p by A8, Satz2p5;
then q,y equiv a,p9 by A3, Satz2p3;
then A21: q,y equiv p9,a by Satz2p5;
( between a,q,y & between x9,p9,a ) by A13, Satz3p2;
then a,y equiv x9,a by A20, A21, Satz2p11;
hence a,y equiv a,x9 by Satz2p5; :: thesis: verum

end;

A22: a,x9 equiv a,y9

proof

q,a equiv a,q9 by A4, Satz2p4;
then p9,x9 equiv a,q9 by A10, Satz2p3;
then A23: x9,p9 equiv a,q9 by Satz2p4;
p,a equiv a,p9 by A3, Satz2p4;
then q9,y9 equiv a,p9 by A12, Satz2p3;
then a,p9 equiv q9,y9 by Satz2p2;
then A24: p9,a equiv q9,y9 by Satz2p4;
( between x9,p9,a & between a,q9,y9 ) by A13, Satz3p2;
then x9,a equiv a,y9 by A23, A24, Satz2p11;
hence a,x9 equiv a,y9 by Satz2p4; :: thesis: verum

end;

A25: x,a,x9,y9 AFS y9,a,y,x

proof

now :: thesis: ( between x,a,x9 & between y9,a,y & a,y9 equiv a,x & x,a equiv y9,a & a,x9 equiv a,y & x,y9 equiv y9,x )

thus between x,a,x9 by A13; :: thesis: ( between y9,a,y & a,y9 equiv a,x & x,a equiv y9,a & a,x9 equiv a,y & x,y9 equiv y9,x )
thus between y9,a,y by A13, Satz3p2; :: thesis: ( a,y9 equiv a,x & x,a equiv y9,a & a,x9 equiv a,y & x,y9 equiv y9,x )
a,x equiv a,x9 by A16, A19, Satz2p3;
then A26: a,x equiv a,y9 by A22, Satz2p3;
hence a,y9 equiv a,x by Satz2p2; :: thesis: ( x,a equiv y9,a & a,x9 equiv a,y & x,y9 equiv y9,x )
a,x equiv y9,a by A26, Satz2p5;
hence x,a equiv y9,a by Satz2p4; :: thesis: ( a,x9 equiv a,y & x,y9 equiv y9,x )
thus a,x9 equiv a,y by A19, Satz2p2; :: thesis: x,y9 equiv y9,x
thus x,y9 equiv y9,x by Satz2p1, Satz2p5; :: thesis: verum

end;

hence x,a,x9,y9 AFS y9,a,y,x ; :: thesis: verum

end;

A27: S is satisfying_SST_A5 ;
x <> a by A13, A2, GTARSKI1:def 10;
then A28: x9,y9 equiv y,x by A27, A25;
A29: y,q,a,x IFS y9,q9,a,x9

proof

now :: thesis: ( between y,q,a & between y9,q9,a & y,a equiv y9,a & q,a equiv q9,a & y,x equiv y9,x9 & a,x equiv a,x9 )

thus ( between y,q,a & between y9,q9,a ) by A13, Satz3p2; :: thesis: ( y,a equiv y9,a & q,a equiv q9,a & y,x equiv y9,x9 & a,x equiv a,x9 )
a,y equiv a,y9 by A19, A22, Satz2p3;
then a,y equiv y9,a by Satz2p5;
hence y,a equiv y9,a by Satz2p4; :: thesis: ( q,a equiv q9,a & y,x equiv y9,x9 & a,x equiv a,x9 )
a,q equiv q9,a by A4, Satz2p5;
hence q,a equiv q9,a by Satz2p4; :: thesis: ( y,x equiv y9,x9 & a,x equiv a,x9 )
y,x equiv x9,y9 by A28, Satz2p2;
hence y,x equiv y9,x9 by Satz2p5; :: thesis: a,x equiv a,x9
thus a,x equiv a,x9 by A16, A19, Satz2p3; :: thesis: verum

end;

hence y,q,a,x IFS y9,q9,a,x9 ; :: thesis: verum

end;

x,p,a,q IFS x9,p9,a,q9

proof

now :: thesis: ( between x,p,a & between x9,p9,a & x,a equiv x9,a & p,a equiv p9,a & x,q equiv x9,q9 & a,q equiv a,q9 )

thus ( between x,p,a & between x9,p9,a ) by A13, Satz3p2; :: thesis: ( x,a equiv x9,a & p,a equiv p9,a & x,q equiv x9,q9 & a,q equiv a,q9 )
a,x equiv a,x9 by A16, A19, Satz2p3;
then a,x equiv x9,a by Satz2p5;
hence x,a equiv x9,a by Satz2p4; :: thesis: ( p,a equiv p9,a & x,q equiv x9,q9 & a,q equiv a,q9 )
a,p equiv p9,a by A3, Satz2p5;
hence p,a equiv p9,a by Satz2p4; :: thesis: ( x,q equiv x9,q9 & a,q equiv a,q9 )
q,x equiv x9,q9 by A29, Satz4p2, Satz2p5;
hence x,q equiv x9,q9 by Satz2p4; :: thesis: a,q equiv a,q9
thus a,q equiv a,q9 by A4; :: thesis: verum

end;

hence x,p,a,q IFS x9,p9,a,q9 ; :: thesis: verum

end;

hence p,q equiv reflection (a,p), reflection (a,q) by Satz4p2; :: thesis: verum

end;

end;