let S be non empty satisfying_Tarski-model TarskiGeometryStruct ; for A, A9 being Subset of S
for x, y being POINT of S st are_orthogonal A,x,A9 & are_orthogonal A,y,A9 holds
x = y
let A, A9 be Subset of S; for x, y being POINT of S st are_orthogonal A,x,A9 & are_orthogonal A,y,A9 holds
x = y
let x, y be POINT of S; ( are_orthogonal A,x,A9 & are_orthogonal A,y,A9 implies x = y )
assume that
A1:
are_orthogonal A,x,A9
and
A2:
are_orthogonal A,y,A9
; x = y
A <> A9
by A1, Satz8p14p1, Satz8p14p2;
hence
x = y
by A1, A2, GTARSKI3:89; verum