for MS being OrtAfPl
for a, b being Element of MS
for A, K being Subset of the carrier of MS st a <> b & ( a,b _|_ K or b,a _|_ K ) & a,b _|_ A holds
K // A