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