for X being OrtAfPl st X is satisfying_AH holds
X is satisfying_TDES