for POS being OrtAfSp
for M, N being Subset of POS
for a, b, c, d being Element of POS st a in M & b in M & c in N & d in N & M _|_ N holds
a,b _|_ c,d