let i, n be Element of NAT ; :: thesis: NEG_MOD (i,n) is_expressible_by n
NEG_MOD (i,n) < 2 to_power n by NAT_D:1, POWER:39;
hence NEG_MOD (i,n) is_expressible_by n by Def3; :: thesis: verum