:: deftheorem Def13 defines _|_ ANALMETR:def 14 :
for POS being non empty ParOrtStr
for K, M being Subset of POS holds
( K _|_ M iff ex p, q being Element of POS st
( p <> q & K = Line (p,q) & p,q _|_ M ) );