let n be Element of NAT ; :: thesis: for X, B being Subset of (TOP-REAL n)
for x being Point of (TOP-REAL n) st x in X holds
B + x c= B (+) X
let X, B be Subset of (TOP-REAL n); :: thesis: for x being Point of (TOP-REAL n) st x in X holds
B + x c= B (+) X
let x be Point of (TOP-REAL n); :: thesis: ( x in X implies B + x c= B (+) X )
assume A1: x in X ; :: thesis: B + x c= B (+) X
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in B + x or y in B (+) X )
assume y in B + x ; :: thesis: y in B (+) X
then consider y1 being Point of (TOP-REAL n) such that
A2: ( y = y1 + x & y1 in B ) ;
thus y in B (+) X by A1, A2; :: thesis: verum