theorem :: CONAFFM:6

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