theorem :: MATHMORP:59

for n being Element of NAT
for X being Subset of (TOP-REAL n) holds 2 (.) X c= X (+) X