let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, a9, b, c being POINT of S st right_angle a,b,c & right_angle a9,b,c & between a,c,a9 holds
b = c
let a, a9, b, c be POINT of S; :: thesis: ( right_angle a,b,c & right_angle a9,b,c & between a,c,a9 implies b = c )
assume ( right_angle a,b,c & right_angle a9,b,c & between a,c,a9 ) ; :: thesis: b = c
then c = reflection (b,c) by GTARSKI3:55;
hence b = c by GTARSKI3:104; :: thesis: verum