Suggestion: Casting theorem for integers

I did not find st. like

i0 is Nat iff ex n being Nat st n <= i0;

for i0 integer;

in INT_1, there is only

 theorem :: INT_1:16 
  0 <= i0 implies i0 is Nat;

-- JosefUrban - 25 Jul 2002

Follow up