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 A9,x,A ) by Satz8p2;