let i1 be Integer; :: thesis: ( 0 < i1 implies 1 <= i1 )
assume A1: 0 < i1 ; :: thesis: 1 <= i1
then reconsider i2 = i1 as Element of NAT by Th3;
0 <> i2 by A1;
hence 1 <= i1 by Lm3; :: thesis: verum