for POS being non empty ParOrtStr
for a, b being Element of POS
for K, M being Subset of POS holds
( ( a,b _|_ K implies K is being_line ) & ( K _|_ M implies ( K is being_line & M is being_line ) ) )