let S be satisfying_Tarski-model TarskiGeometryStruct ; 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; 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 A2:
p <> a
;
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;
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;
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;
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;
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;
verum
end; A25:
x,
a,
x9,
y9 AFS y9,
a,
y,
x
proof
now ( 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;
( 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;
( 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;
( 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;
( a,x9 equiv a,y & x,y9 equiv y9,x )thus
a,
x9 equiv a,
y
by A19, Satz2p2;
x,y9 equiv y9,xthus
x,
y9 equiv y9,
x
by Satz2p1, Satz2p5;
verum end;
hence
x,
a,
x9,
y9 AFS y9,
a,
y,
x
;
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 ( 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;
( 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;
( 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;
( 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;
a,x equiv a,x9thus
a,
x equiv a,
x9
by A16, A19, Satz2p3;
verum end;
hence
y,
q,
a,
x IFS y9,
q9,
a,
x9
;
verum
end;
x,
p,
a,
q IFS x9,
p9,
a,
q9
proof
now ( 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;
( 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;
( 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;
( 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;
a,q equiv a,q9thus
a,
q equiv a,
q9
by A4;
verum end;
hence
x,
p,
a,
q IFS x9,
p9,
a,
q9
;
verum
end; hence
p,
q equiv reflection (
a,
p),
reflection (
a,
q)
by Satz4p2;
verum end; end;