for MS being OrtAfPl
for o, c, c1, a being Element of MS st not LIN o,c,a holds
ex a1 being Element of MS st
( o,a _|_ o,a1 & c,a _|_ c1,a1 )