let n be Element of NAT ; :: thesis: for X being non empty Subset of (TOP-REAL n) holds 0 (.) X = {(0. (TOP-REAL n))}
let X be non empty Subset of (TOP-REAL n); :: thesis: 0 (.) X = {(0. (TOP-REAL n))}
thus 0 (.) X c= {(0. (TOP-REAL n))} :: according to XBOOLE_0:def 10 :: thesis: {(0. (TOP-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. (TOP-REAL n))} )
assume x in 0 (.) X ; :: thesis: x in {(0. (TOP-REAL n))}
then consider a being Point of (TOP-REAL n) such that
A1: ( x = 0 * a & a in X ) ;
x = 0. (TOP-REAL n) by A1, EUCLID:33;
hence x in {(0. (TOP-REAL n))} by ZFMISC_1:37; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(0. (TOP-REAL n))} or x in 0 (.) X )
assume x in {(0. (TOP-REAL n))} ; :: thesis: x in 0 (.) X
then {x} c= {(0. (TOP-REAL n))} by ZFMISC_1:37;
then A2: x = 0. (TOP-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