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