theorem :: CONMETR:12

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