let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: for a, b, c, p being POINT of S st right_angle a,b,c & Middle reflection (a,c),p, reflection (b,c) holds
( right_angle b,a,p & ( b <> c implies a <> p ) )
let a, b, c, p be POINT of S; :: thesis: ( right_angle a,b,c & Middle reflection (a,c),p, reflection (b,c) implies ( right_angle b,a,p & ( b <> c implies a <> p ) ) )
assume that
A1: right_angle a,b,c and
A2: Middle reflection (a,c),p, reflection (b,c) ; :: thesis: ( right_angle b,a,p & ( b <> c implies a <> p ) )
set d = reflection (b,c);
set b9 = reflection (a,b);
set c9 = reflection (a,c);
set d9 = reflection (a,(reflection (b,c)));
set p9 = reflection (a,p);
A3: right_angle reflection (a,b),b,c

proof

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

suppose a = b ; :: thesis: right_angle reflection (a,b),b,c

then reflection (a,b) = b by GTARSKI3:104;
hence right_angle reflection (a,b),b,c by Satz8p2, Satz8p5; :: thesis: verum

end;

suppose A4: a <> b ; :: thesis: right_angle reflection (a,b),b,c

Middle b,a, reflection (a,b) by GTARSKI3:def 13;
then between b,a, reflection (a,b) by GTARSKI3:def 12;
then Collinear b,a, reflection (a,b) by GTARSKI1:def 17;
hence right_angle reflection (a,b),b,c by A1, A4, Satz8p3; :: thesis: verum

end;

end;

end;

A5: reflection (a,b),b equiv b, reflection (a,b)

proof

reflection (a,b),b equiv reflection (a,(reflection (a,b))), reflection (a,b) by GTARSKI3:105;
hence reflection (a,b),b equiv b, reflection (a,b) by GTARSKI3:101; :: thesis: verum

end;

A6: reflection (a,b),c equiv b, reflection (a,c)

proof

reflection (a,b),c equiv reflection (a,(reflection (a,b))), reflection (a,c) by GTARSKI3:105;
hence reflection (a,b),c equiv b, reflection (a,c) by GTARSKI3:101; :: thesis: verum

end;

reflection (a,b),b,c cong b, reflection (a,b), reflection (a,c)

proof

b,c equiv reflection (a,b), reflection (a,c) by GTARSKI3:105;
hence reflection (a,b),b,c cong b, reflection (a,b), reflection (a,c) by A5, A6, GTARSKI1:def 3; :: thesis: verum

end;

then A7: right_angle b, reflection (a,b), reflection (a,c) by A3, Satz8p10;
A8: reflection ((reflection (a,b)),(reflection (a,c))) = reflection (a,(reflection (b,c))) by Prelim12, GTARSKI3:100;
reflection (a,c),p, reflection (b,c),b IFS reflection (a,(reflection (b,c))), reflection (a,p),c,b

proof

now :: thesis: ( between reflection (a,c),p, reflection (b,c) & between reflection (a,(reflection (b,c))), reflection (a,p),c & reflection (a,c), reflection (b,c) equiv reflection (a,(reflection (b,c))),c & p, reflection (b,c) equiv reflection (a,p),c & reflection (a,c),b equiv reflection (a,(reflection (b,c))),b & reflection (b,c),b equiv c,b )

thus between reflection (a,c),p, reflection (b,c) by A2, GTARSKI3:def 12; :: thesis: ( between reflection (a,(reflection (b,c))), reflection (a,p),c & reflection (a,c), reflection (b,c) equiv reflection (a,(reflection (b,c))),c & p, reflection (b,c) equiv reflection (a,p),c & reflection (a,c),b equiv reflection (a,(reflection (b,c))),b & reflection (b,c),b equiv c,b )
between reflection (b,c),p, reflection (a,c) by A2, GTARSKI3:14, GTARSKI3:def 12;
then between reflection (a,(reflection (b,c))), reflection (a,p), reflection (a,(reflection (a,c))) by GTARSKI3:106;
hence between reflection (a,(reflection (b,c))), reflection (a,p),c by GTARSKI3:101; :: thesis: ( reflection (a,c), reflection (b,c) equiv reflection (a,(reflection (b,c))),c & p, reflection (b,c) equiv reflection (a,p),c & reflection (a,c),b equiv reflection (a,(reflection (b,c))),b & reflection (b,c),b equiv c,b )
reflection (a,c), reflection (b,c) equiv reflection (a,(reflection (a,c))), reflection (a,(reflection (b,c))) by GTARSKI3:105;
then reflection (a,c), reflection (b,c) equiv c, reflection (a,(reflection (b,c))) by GTARSKI3:101;
hence reflection (a,c), reflection (b,c) equiv reflection (a,(reflection (b,c))),c by GTARSKI3:7; :: thesis: ( p, reflection (b,c) equiv reflection (a,p),c & reflection (a,c),b equiv reflection (a,(reflection (b,c))),b & reflection (b,c),b equiv c,b )

now :: thesis: ( p, reflection (b,c) equiv reflection (a,p), reflection (a,(reflection (b,c))) & reflection (a,p), reflection (a,(reflection (b,c))) equiv reflection (a,p),c )

thus p, reflection (b,c) equiv reflection (a,p), reflection (a,(reflection (b,c))) by GTARSKI3:105; :: thesis: reflection (a,p), reflection (a,(reflection (b,c))) equiv reflection (a,p),c
A9: p, reflection (a,c) equiv p, reflection (b,c) by A2, GTARSKI3:def 12;
p, reflection (a,c) equiv reflection (a,p), reflection (a,(reflection (a,c))) by GTARSKI3:105;
then A10: p, reflection (a,c) equiv reflection (a,p),c by GTARSKI3:101;
p, reflection (b,c) equiv reflection (a,p), reflection (a,(reflection (b,c))) by GTARSKI3:105;
then p, reflection (a,c) equiv reflection (a,p), reflection (a,(reflection (b,c))) by A9, GTARSKI3:5;
then reflection (a,p), reflection (a,(reflection (b,c))) equiv p, reflection (a,c) by GTARSKI3:4;
hence reflection (a,p), reflection (a,(reflection (b,c))) equiv reflection (a,p),c by A10, GTARSKI3:5; :: thesis: verum

end;

hence p, reflection (b,c) equiv reflection (a,p),c by GTARSKI3:5; :: thesis: ( reflection (a,c),b equiv reflection (a,(reflection (b,c))),b & reflection (b,c),b equiv c,b )
reflection (a,c),b equiv b, reflection (a,(reflection (b,c))) by A8, A7, GTARSKI3:6;
hence reflection (a,c),b equiv reflection (a,(reflection (b,c))),b by GTARSKI3:7; :: thesis: reflection (b,c),b equiv c,b
Middle c,b, reflection (b,c) by GTARSKI3:def 13;
then b, reflection (b,c) equiv b,c by GTARSKI3:4, GTARSKI3:def 12;
then reflection (b,c),b equiv b,c by GTARSKI3:6;
hence reflection (b,c),b equiv c,b by GTARSKI3:7; :: thesis: verum

end;

hence reflection (a,c),p, reflection (b,c),b IFS reflection (a,(reflection (b,c))), reflection (a,p),c,b by GTARSKI3:def 5; :: thesis: verum

end;

then b,p equiv reflection (a,p),b by GTARSKI3:6, GTARSKI3:41;
hence right_angle b,a,p by GTARSKI3:7; :: thesis: ( b <> c implies a <> p )
thus ( b <> c implies a <> p ) :: thesis: verum

proof

assume A11: b <> c ; :: thesis: a <> p
assume A12: a = p ; :: thesis: contradiction
c = reflection (a,(reflection (a,c))) by GTARSKI3:101
.= reflection (b,c) by A12, A2, GTARSKI3:def 13 ;
then Middle c,b,c by GTARSKI3:def 13;
hence contradiction by GTARSKI3:97, A11; :: thesis: verum

end;