theorem :: CONMETR:11

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