theorem Th3: :: CONAFFM:3

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