theorem Th1: :: FSM_3:1

for i, k, l being Nat st i >= k + l holds
i >= k