let i1, i2 be Integer; :: thesis: ( i2 <= i1 implies i1 - i2 in NAT )
assume i2 <= i1 ; :: thesis: i1 - i2 in NAT
then i2 - i2 <= i1 - i2 by XREAL_1:9;
hence i1 - i2 in NAT by Th3; :: thesis: verum