:: deftheorem defines being_line ANALMETR:def 12 :
for POS being non empty ParOrtStr
for A being Subset of POS holds
( A is being_line iff ex a, b being Element of POS st
( a <> b & A = Line (a,b) ) );