theorem Th1: :: JORDAN5B:1

for i1 being Nat st 1 <= i1 holds
i1 -' 1 < i1