let i2, i1 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:11;
hence i1 - i2 in NAT by Th16; :: thesis: verum