let S be non empty satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: x = y
A <> A9 by A1, Satz8p14p1, Satz8p14p2;
hence x = y by A1, A2, GTARSKI3:89; :: thesis: verum