for X being OrtAfPl st X is satisfying_OSCH & X is satisfying_TDES holds
X is satisfying_SCH