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 a,b, reflection (b,c)
let a, b, c be POINT of S; :: thesis: ( right_angle a,b,c implies right_angle a,b, reflection (b,c) )
assume right_angle a,b,c ; :: thesis: right_angle a,b, reflection (b,c)
then a, reflection (b,c) equiv a,c by GTARSKI3:4;
hence right_angle a,b, reflection (b,c) by GTARSKI3:101; :: thesis: verum