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