:: deftheorem defines _|_ ANALMETR:def 5 :
for POS being OrtStr
for a, b, c, d being Element of POS holds
( a,b _|_ c,d iff [[a,b],[c,d]] in the orthogonality of POS );