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