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

now

given y being set such that A2: y in X + x ; :: thesis: contradiction
ex y1 being Point of (TOP-REAL n) st
( y = y1 + x & y1 in X ) by A2;
hence contradiction by A1; :: thesis: verum

end;

hence X + x = {} by XBOOLE_0:def 1; :: thesis: verum