let n be Element of NAT ; :: thesis: for X being non empty Subset of (TOP-REAL n) holds 0 (.) X = {(0. (TOP-REAL n))}
set T = 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 object ; :: 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 ex a being Point of (TOP-REAL n) st
( x = 0 * a & a in X ) ;
then x = 0. (TOP-REAL n) by RLVECT_1:10;
hence x in {(0. (TOP-REAL n))} by ZFMISC_1:31; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(0. (TOP-REAL n))} or x in 0 (.) X )
set d = the Element of X;
reconsider d1 = the Element of X as Point of (TOP-REAL n) ;
assume x in {(0. (TOP-REAL n))} ; :: thesis: x in 0 (.) X
then {x} c= {(0. (TOP-REAL n))} by ZFMISC_1:31;
then x = 0. (TOP-REAL n) by ZFMISC_1:18;
then x = 0 * d1 by RLVECT_1:10;
hence x in 0 (.) X ; :: thesis: verum