let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b being POINT of S holds right_angle a,b,b
let a, b be POINT of S; :: thesis: right_angle a,b,b
a,b equiv a,b by GTARSKI3:2;
hence right_angle a,b,b by Lem01; :: thesis: verum