theorem :: CONMETR:10

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