set IT = { (2 to_power n) where n is Element of NAT : verum } ;

A1: now :: thesis: for x being object st x in { (2 to_power n) where n is Element of NAT : verum } holds
x in NAT

let x be object ; :: thesis: ( x in { (2 to_power n) where n is Element of NAT : verum } implies x in NAT )
assume x in { (2 to_power n) where n is Element of NAT : verum } ; :: thesis: x in NAT
then ex n being Element of NAT st 2 to_power n = x ;
hence x in NAT ; :: thesis: verum

end;

2 to_power 1 in { (2 to_power n) where n is Element of NAT : verum } ;
hence { (2 to_power n) where n is Element of NAT : verum } is non empty Subset of NAT by A1, TARSKI:def 3; :: thesis: verum