for POS being OrtAfSp
for K being Subset of POS
for a, b being Element of POS st a,b _|_ K holds
b,a _|_ K