for S being non empty satisfying_Tarski-model TarskiGeometryStruct
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 ) )