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