for POS being OrtAfSp
for A, K, M, N being Subset of POS
for a, b, p being Element of POS st p in M & p in N & a in M & b in N & a <> b & a in K & b in K & A _|_ M & A _|_ N & K is being_line holds
A _|_ K