let n be Element of NAT ; :: thesis: for X being Subset of (TOP-REAL n) st X = {} holds
0 (.) X = {}
let X be Subset of (TOP-REAL n); :: thesis: ( X = {} implies 0 (.) X = {} )
assume A1: X = {} ; :: thesis: 0 (.) X = {}

now

given x being set such that A2: x in 0 (.) X ; :: thesis: contradiction
consider a being Point of (TOP-REAL n) such that
A3: ( x = 0 * a & a in X ) by A2;
thus contradiction by A1, A3; :: thesis: verum

end;

hence 0 (.) X = {} by XBOOLE_0:def 1; :: thesis: verum