:: deftheorem defines are_orthogonal GTARSKI4:def 2 :
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 ( A is_line & A9 is_line & x in A & x in A9 & ( for u, v being POINT of S st u in A & v in A9 holds
right_angle u,x,v ) ) );