let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, a9, b, b9, c, c9 being POINT of S st right_angle a,b,c & a,b,c cong a9,b9,c9 holds
right_angle a9,b9,c9
let a, a9, b, b9, c, c9 be POINT of S; :: thesis: ( right_angle a,b,c & a,b,c cong a9,b9,c9 implies right_angle a9,b9,c9 )
assume that
A1: right_angle a,b,c and
A2: a,b,c cong a9,b9,c9 ; :: thesis: right_angle a9,b9,c9

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

suppose b = c ; :: thesis: right_angle a9,b9,c9

then ( a,b equiv a9,b9 & a,b equiv a9,c9 & b,b equiv b9,c9 ) by A2, GTARSKI1:def 3;
then b9 = c9 by GTARSKI1:def 7, GTARSKI3:4;
hence right_angle a9,b9,c9 by Satz8p5; :: thesis: verum

end;

suppose A3: b <> c ; :: thesis: right_angle a9,b9,c9

set d = reflection (b,c);
set d9 = reflection (b9,c9);
A4: ( a,b equiv a9,b9 & a,c equiv a9,c9 & b,c equiv b9,c9 ) by A2, GTARSKI1:def 3;

now :: thesis: ( between c,b, reflection (b,c) & between c9,b9, reflection (b9,c9) & b,a equiv b9,a9 & c,b equiv c9,b9 & c,a equiv c9,a9 & b, reflection (b,c) equiv b9, reflection (b9,c9) )

( Middle c,b, reflection (b,c) & Middle c9,b9, reflection (b9,c9) ) by GTARSKI3:def 13;
hence ( between c,b, reflection (b,c) & between c9,b9, reflection (b9,c9) ) by GTARSKI3:def 12; :: thesis: ( b,a equiv b9,a9 & c,b equiv c9,b9 & c,a equiv c9,a9 & b, reflection (b,c) equiv b9, reflection (b9,c9) )
thus ( b,a equiv b9,a9 & c,b equiv c9,b9 & c,a equiv c9,a9 ) by A4, Prelim01; :: thesis: b, reflection (b,c) equiv b9, reflection (b9,c9)
b,c equiv reflection (b,b), reflection (b,c) by GTARSKI3:105;
then A5: b9,c9 equiv reflection (b,b), reflection (b,c) by A4, GTARSKI1:def 6;
b9,c9 equiv reflection (b9,b9), reflection (b9,c9) by GTARSKI3:105;
then reflection (b,b), reflection (b,c) equiv reflection (b9,b9), reflection (b9,c9) by A5, GTARSKI1:def 6;
then b, reflection (b,c) equiv reflection (b9,b9), reflection (b9,c9) by GTARSKI3:104;
hence b, reflection (b,c) equiv b9, reflection (b9,c9) by GTARSKI3:104; :: thesis: verum

end;

then c,b, reflection (b,c),a AFS c9,b9, reflection (b9,c9),a9 by GTARSKI3:def 2;
then A6: a, reflection (b,c) equiv reflection (b9,c9),a9 by A3, GTARSKI3:6, GTARSKI3:10;
a,c equiv reflection (b9,c9),a9 by A1, A6, Prelim03;
hence right_angle a9,b9,c9 by A4, Prelim03; :: thesis: verum

end;

end;