theorem :: GTARSKI4:16

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c being POINT of S st right_angle a,b,c holds
right_angle a,b, reflection (b,c)