for MS being OrtAfPl
for o, a, a1, b, b1, c, c1 being Element of MS st o,b _|_ o,b1 & o,c _|_ o,c1 & a,b _|_ a1,b1 & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b & o = a1 holds
b,c _|_ b1,c1