for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for A, A9 being Subset of S st are_orthogonal A,A9 holds
A <> A9