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