theorem :: CONAFFM:4

for X being OrtAfPl st X is satisfying_LIN1 holds
X is satisfying_LIN2