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

proof

let p be set ; :: according to TARSKI:def 3 :: thesis: ( not p in X (-) B or p in Y (-) B )
assume p in X (-) B ; :: thesis: p in Y (-) B
then consider p1 being Point of (TOP-REAL n) such that
A2: p = p1 and
A3: B + p1 c= X ;
B + p1 c= Y by A1, A3, XBOOLE_1:1;
hence p in Y (-) B by A2; :: thesis: verum

end;

let p be set ; :: according to TARSKI:def 3 :: thesis: ( not p in X (+) B or p in Y (+) B )
assume p in X (+) B ; :: thesis: p in Y (+) B
then ex p1, p2 being Point of (TOP-REAL n) st
( p = p1 + p2 & p1 in X & p2 in B ) ;
hence p in Y (+) B by A1; :: thesis: verum