theorem :: CONMETR:15

for X being OrtAfPl st X is satisfying_3H holds
X is satisfying_OPAP