let S be satisfying_Tarski-model TarskiGeometryStruct ; for a, b, c being POINT of S st right_angle a,b,c holds
right_angle c,b,a
let a, b, c be POINT of S; ( right_angle a,b,c implies right_angle c,b,a )
assume
right_angle a,b,c
; right_angle c,b,a
then A1:
c,a equiv a, reflection (b,c)
by GTARSKI3:6;
a, reflection (b,c) equiv reflection (b,a), reflection (b,(reflection (b,c)))
by GTARSKI3:105;
then
a, reflection (b,c) equiv reflection (b,a),c
by GTARSKI3:101;
then
a, reflection (b,c) equiv c, reflection (b,a)
by GTARSKI3:7;
hence
right_angle c,b,a
by A1, GTARSKI3:5; verum