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

proof

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

end;

let p be set ; :: according to TARSKI:def 3 :: thesis: ( not p in X (+) B1 or p in X (+) B2 )
assume p in X (+) B1 ; :: thesis: p in X (+) B2
then consider x, b being Point of (TOP-REAL n) such that
A3: ( p = x + b & x in X & b in B1 ) ;
thus p in X (+) B2 by A1, A3; :: thesis: verum