theorem :: CONMETR:14

for X being OrtAfPl st X is satisfying_MH1 & X is satisfying_MH2 holds
X is satisfying_OPAP