let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: 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; :: thesis: ( right_angle a,b,c implies right_angle c,b,a )
assume right_angle a,b,c ; :: thesis: 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; :: thesis: verum