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