:: deftheorem Def10 defines Line ANALMETR:def 11 :
for POS being non empty ParOrtStr
for a, b being Element of POS
for b₄ being Subset of POS holds
( b₄ = Line (a,b) iff for x being Element of POS holds
( x in b₄ iff LIN a,b,x ) );