let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c being POINT of S st right_angle a,b,c & right_angle a,c,b holds
b = c
let a, b, c be POINT of S; :: thesis: ( right_angle a,b,c & right_angle a,c,b implies b = c )
assume that
A1: right_angle a,b,c and
A2: right_angle a,c,b ; :: thesis: b = c
assume A3: b <> c ; :: thesis: contradiction
set c9 = reflection (b,c);
set a9 = reflection (c,a);

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

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

proof

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

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

thus a, reflection (b,c) equiv a,c by A1, GTARSKI3:4; :: thesis: a,c equiv reflection (c,a),c
right_angle c,c,a by Satz8p2, Satz8p5;
hence a,c equiv reflection (c,a),c by Prelim01; :: thesis: verum

end;

hence a, reflection (b,c) equiv reflection (c,a),c by GTARSKI3:5; :: thesis: a, reflection (b,c) equiv reflection (c,a), reflection (b,c)

now :: thesis: ( right_angle b,c,a & b <> c & Collinear c,b, reflection (b,c) )

thus right_angle b,c,a by A2, Satz8p2; :: thesis: ( b <> c & Collinear c,b, reflection (b,c) )
thus b <> c by A3; :: thesis: Collinear c,b, reflection (b,c)
Middle c,b, reflection (b,c) by GTARSKI3:def 13;
hence Collinear c,b, reflection (b,c) by Prelim08a; :: thesis: verum

end;

then right_angle reflection (b,c),c,a by Satz8p3;
then A4: right_angle a,c, reflection (b,c) by Satz8p2;
a, reflection (c,(reflection (b,c))) equiv reflection (c,a), reflection (c,(reflection (c,(reflection (b,c))))) by GTARSKI3:105;
then a, reflection (b,c) equiv reflection (c,a), reflection (c,(reflection (c,(reflection (b,c))))) by A4, GTARSKI3:5;
hence a, reflection (b,c) equiv reflection (c,a), reflection (b,c) by GTARSKI3:101; :: thesis: verum

end;

hence reflection (c,a),c equiv reflection (c,a), reflection (b,c) by GTARSKI1:def 6; :: thesis: verum

end;

hence right_angle reflection (c,a),b,c ; :: thesis: between a,c, reflection (c,a)
Middle a,c, reflection (c,a) by GTARSKI3:def 13;
hence between a,c, reflection (c,a) by GTARSKI3:def 12; :: thesis: verum

end;

hence contradiction by A1, A3, Satz8p6; :: thesis: verum