let n be Element of NAT ; :: thesis: for X, B being Subset of (TOP-REAL n) holds (X (-) B) ` = (X ` ) (+) (B ! )
let X, B be Subset of (TOP-REAL n); :: thesis: (X (-) B) ` = (X ` ) (+) (B ! )
thus (X (-) B) ` c= (X ` ) (+) (B ! ) :: according to XBOOLE_0:def 10 :: thesis: (X ` ) (+) (B ! ) c= (X (-) B) `

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (X (-) B) ` or x in (X ` ) (+) (B ! ) )
assume A1: x in (X (-) B) ` ; :: thesis: x in (X ` ) (+) (B ! )
then A2: ( x in the carrier of (TOP-REAL n) & not x in X (-) B ) by XBOOLE_0:def 5;
reconsider x1 = x as Point of (TOP-REAL n) by A1;
not B + x1 c= X by A2;
then B + x1 meets X ` by SUBSET_1:44;
then consider y being set such that
A3: ( y in B + x1 & y in X ` ) by XBOOLE_0:3;
consider b1 being Point of (TOP-REAL n) such that
A4: ( y = b1 + x1 & b1 in B ) by A3;
reconsider y1 = y as Point of (TOP-REAL n) by A3;
x1 = y1 - b1 by A4, EUCLID:52;
then A5: x1 = y1 + (- b1) by EUCLID:45;
- b1 in B ! by A4;
hence x in (X ` ) (+) (B ! ) by A3, A5; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (X ` ) (+) (B ! ) or x in (X (-) B) ` )
assume x in (X ` ) (+) (B ! ) ; :: thesis: x in (X (-) B) `
then consider x1, b1 being Point of (TOP-REAL n) such that
A6: ( x = x1 + b1 & x1 in X ` & b1 in B ! ) ;
reconsider xx = x as Point of (TOP-REAL n) by A6;
consider q being Point of (TOP-REAL n) such that
A7: ( b1 = - q & q in B ) by A6;
xx = x1 - q by A6, A7, EUCLID:45;
then A8: xx + q = x1 by EUCLID:52;
q + xx in { (q1 + xx) where q1 is Point of (TOP-REAL n) : q1 in B } by A7;
then A9: B + xx meets X ` by A6, A8, XBOOLE_0:3;
not xx in X (-) B

proof

assume xx in X (-) B ; :: thesis: contradiction
then consider yy being Point of (TOP-REAL n) such that
A10: ( xx = yy & B + yy c= X ) ;
thus contradiction by A9, A10, SUBSET_1:44; :: thesis: verum

end;

hence x in (X (-) B) ` by XBOOLE_0:def 5; :: thesis: verum