for POS being OrtAfSp
for K, M, N being Subset of POS st K _|_ M & K // N holds
N _|_ M