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