for POS being OrtAfSp
for K, M being Subset of POS
for r, s being Element of POS st r,s _|_ K & K // M holds
r,s _|_ M