let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b being POINT of S st right_angle a,b,a holds
a = b
let a, b be POINT of S; :: thesis: ( right_angle a,b,a implies a = b )
assume A1: right_angle a,b,a ; :: thesis: a = b
right_angle a,a,b by Satz8p2, Satz8p5;
hence a = b by A1, Satz8p7; :: thesis: verum