theorem :: CONMETR:9

for X being OrtAfPl st X is satisfying_MH1 holds
X is satisfying_OSCH