:: deftheorem defines LIN ANALMETR:def 10 :
for POS being non empty ParOrtStr
for a, b, c being Element of POS holds
( LIN a,b,c iff a,b // a,c );