theorem :: CONAFFM:2

for X being OrtAfPl st X is satisfying_ODES holds
X is satisfying_AH ;