let n be Element of NAT ; :: thesis: for X being Subset of (TOP-REAL n) holds 2 (.) X c= X (+) X
let X be Subset of (TOP-REAL n); :: thesis: 2 (.) X c= X (+) X
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in 2 (.) X or x in X (+) X )
assume x in 2 (.) X ; :: thesis: x in X (+) X
then consider z being Point of (TOP-REAL n) such that
A1: ( x = 2 * z & z in X ) ;
x = (1 + 1) * z by A1
.= (1 * z) + (1 * z) by EUCLID:37
.= z + (1 * z) by EUCLID:33
.= z + z by EUCLID:33 ;
hence x in X (+) X by A1; :: thesis: verum