theorem :: CONMETR:13

for X being OrtAfPl st X is satisfying_OPAP & X is satisfying_DES holds
X is satisfying_PAP