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 object ; :: 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 and
A2: z in X ;
x = (1 + 1) * z by A1
.= (1 * z) + (1 * z) by RLVECT_1:def 6
.= z + (1 * z) by RLVECT_1:def 8
.= z + z by RLVECT_1:def 8 ;
hence x in X (+) X by A2; :: thesis: verum