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