let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, a9, b, c being POINT of S st right_angle a,b,c & a <> b & Collinear b,a,a9 holds
right_angle a9,b,c
let a, a9, b, c be POINT of S; :: thesis: ( right_angle a,b,c & a <> b & Collinear b,a,a9 implies right_angle a9,b,c )
assume that
A1: right_angle a,b,c and
A2: a <> b and
A3: Collinear b,a,a9 ; :: thesis: right_angle a9,b,c

now :: thesis: b,c equiv b, reflection (b,c)

b,c equiv reflection (b,b), reflection (b,c) by GTARSKI3:105;
hence b,c equiv b, reflection (b,c) by Lem01; :: thesis: verum

end;

hence right_angle a9,b,c by A1, A2, A3, GTARSKI3:53; :: thesis: verum