i < 2 to_power n by A1, Def3;
then (2 to_power n) - i > i - i by XREAL_1:11;
hence (2 to_power n) - i is Element of NAT by INT_1:16; :: thesis: verum