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