let n be Element of NAT ; :: thesis: for B, X being Subset of (TOP-REAL n) st 0. (TOP-REAL n) in B holds
( X (-) B c= X & X c= X (+) B )
let B, X be Subset of (TOP-REAL n); :: thesis: ( 0. (TOP-REAL n) in B implies ( X (-) B c= X & X c= X (+) B ) )
assume A1: 0. (TOP-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 and
A3: B + p1 c= X ;
(0. (TOP-REAL n)) + p1 in { (q + p1) where q is Point of (TOP-REAL n) : q in B } by A1;
then (0. (TOP-REAL n)) + p1 in X by A3;
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 A4: p in X ; :: thesis: p in X (+) B
then reconsider p = p as Point of (TOP-REAL n) ;
p + (0. (TOP-REAL n)) in { (x + b) where x, b is Point of (TOP-REAL n) : ( x in X & b in B ) } by A1, A4;
hence p in X (+) B by EUCLID:31; :: thesis: verum