let n be Element of NAT ; :: thesis: for B, X being Subset of (TOP-REAL n) st 0.REAL n in B holds
( X (-) B c= X & X c= X (+) B )
let B, X be Subset of (TOP-REAL n); :: thesis: ( 0.REAL n in B implies ( X (-) B c= X & X c= X (+) B ) )
assume A1: 0.REAL n in B ; :: thesis: ( X (-) B c= X & X c= X (+) B )
thus X (-) B c= X :: thesis: X c= X (+) B

proof

let p be set ; :: according to TARSKI:def 3 :: thesis: ( not p in X (-) B or p in X )
assume p in X (-) B ; :: thesis: p in X
then consider p1 being Point of (TOP-REAL n) such that
A2: ( p = p1 & B + p1 c= X ) ;
(0.REAL n) + p1 in { (q + p1) where q is Point of (TOP-REAL n) : q in B } by A1;
then (0.REAL n) + p1 in X by A2;
hence p in X by A2, EUCLID:31; :: thesis: verum

end;

let p be set ; :: according to TARSKI:def 3 :: thesis: ( not p in X or p in X (+) B )
assume A3: p in X ; :: thesis: p in X (+) B
then reconsider p = p as Point of (TOP-REAL n) ;
p + (0.REAL n) in { (x + b) where x, b is Point of (TOP-REAL n) : ( x in X & b in B ) } by A1, A3;
hence p in X (+) B by EUCLID:31; :: thesis: verum