:: deftheorem defines are_lorthogonal GTARSKI4:def 4 :
for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for A being Subset of S
for x, c, d being POINT of S holds
( are_lorthogonal A,x,c,d iff ( c <> d & are_orthogonal A,x, Line (c,d) ) );