:: deftheorem defines are_orthogonal GTARSKI4:def 3 :
for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for A, A9 being Subset of S holds
( are_orthogonal A,A9 iff ex x being POINT of S st are_orthogonal A,x,A9 );