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 and
A2: y1 in X (-) B and
A3: y2 in B ;
consider y being Point of (TOP-REAL n) such that
A4: y1 = y and
A5: B + y c= X by A2;
x in B + y by A1, A3, A4;
hence x in X by A5; :: thesis: verum