theorem :: CONAFFM:1

for X being OrtAfPl st X is satisfying_ODES holds
X is satisfying_DES