let n be Element of NAT ; :: thesis: for X, B being Subset of (TOP-REAL n) holds (X (-) B) (+) B c= X
let X, B be Subset of (TOP-REAL n); :: thesis: (X (-) B) (+) B c= X
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (X (-) B) (+) B or x in X )
assume x in (X (-) B) (+) B ; :: thesis: x in X
then consider y1, y2 being Point of (TOP-REAL n) such that
A1: ( x = y1 + y2 & y1 in X (-) B & y2 in B ) ;
consider y being Point of (TOP-REAL n) such that
A2: ( y1 = y & B + y c= X ) by A1;
x in B + y by A1, A2;
hence x in X by A2; :: thesis: verum