:: deftheorem defines satisfying_ODES CONAFFM:def 4 :
for X being OrtAfPl holds
( X is satisfying_ODES iff for o, a, a1, b, b1, c, c1 being Element of X st o,a _|_ o,a1 & 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 holds
b,c _|_ b1,c1 );