let S be non empty satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for A, A9 being Subset of S
for x being POINT of S holds
( are_orthogonal A,x,A9 iff ( are_orthogonal A,A9 & A,A9 Is x ) )
let A, A9 be Subset of S; :: thesis: for x being POINT of S holds
( are_orthogonal A,x,A9 iff ( are_orthogonal A,A9 & A,A9 Is x ) )
let x be POINT of S; :: thesis: ( are_orthogonal A,x,A9 iff ( are_orthogonal A,A9 & A,A9 Is x ) )

hereby :: thesis: ( are_orthogonal A,A9 & A,A9 Is x implies are_orthogonal A,x,A9 )

assume A1: are_orthogonal A,x,A9 ; :: thesis: ( are_orthogonal A,A9 & A,A9 Is x )
hence are_orthogonal A,A9 ; :: thesis: A,A9 Is x
hence A,A9 Is x by A1, Satz8p14p1; :: thesis: verum

end;

assume A2: ( are_orthogonal A,A9 & A,A9 Is x ) ; :: thesis: are_orthogonal A,x,A9
then ex y being POINT of S st are_orthogonal A,y,A9 ;
hence are_orthogonal A,x,A9 by A2, GTARSKI3:88; :: thesis: verum