let n be Element of NAT ; :: thesis: for X being non empty Subset of (TOP-REAL n) holds 0 (.) X = {(0.REAL n)}
let X be non empty Subset of (TOP-REAL n); :: thesis: 0 (.) X = {(0.REAL n)}
thus 0 (.) X c= {(0.REAL n)} :: according to XBOOLE_0:def 10 :: thesis: {(0.REAL n)} c= 0 (.) X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in 0 (.) X or x in {(0.REAL n)} )
assume x in 0 (.) X ; :: thesis: x in {(0.REAL n)}
then consider a being Point of (TOP-REAL n) such that
A1: ( x = 0 * a & a in X ) ;
x = 0.REAL n by A1, EUCLID:33;
hence x in {(0.REAL n)} by ZFMISC_1:37; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(0.REAL n)} or x in 0 (.) X )
assume x in {(0.REAL n)} ; :: thesis: x in 0 (.) X
then {x} c= {(0.REAL n)} by ZFMISC_1:37;
then A2: x = 0.REAL n by ZFMISC_1:24;
consider d being Element of X;
reconsider d1 = d as Point of (TOP-REAL n) ;
x = 0 * d1 by A2, EUCLID:33;
hence x in 0 (.) X ; :: thesis: verum