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:43;
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 ! ) ;
consider b2 being Point of (TOP-REAL n) such that
A7: ( b1 = - b2 & b2 in B ) by A6;
A8: x = x1 - b2 by A6, A7, EUCLID:45;
reconsider xx = x as Point of (TOP-REAL n) by A6;
A9: xx + b2 = x1 by A8, EUCLID:52;
b2 + xx in { (pb + xx) where pb is Point of (TOP-REAL n) : pb in B } by A7;
then A10: B + xx meets X by A6, A9, 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
A11: ( xx = yy & B + yy c= X ` ) ;
thus contradiction by A10, A11, SUBSET_1:43; :: thesis: verum

end;

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