let n be Element of NAT ; :: thesis: for X, Y, B being Subset of (TOP-REAL n) holds (X /\ Y) (+) B c= (X (+) B) /\ (Y (+) B)
let X, Y, B be Subset of (TOP-REAL n); :: thesis: (X /\ Y) (+) B c= (X (+) B) /\ (Y (+) B)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (X /\ Y) (+) B or x in (X (+) B) /\ (Y (+) B) )
assume x in (X /\ Y) (+) B ; :: thesis: x in (X (+) B) /\ (Y (+) B)
then consider y1, y2 being Point of (TOP-REAL n) such that
A1: ( x = y1 + y2 & y1 in X /\ Y & y2 in B ) ;
( y1 in X & y1 in Y ) by A1, XBOOLE_0:def 4;
then ( x in { (y3 + y4) where y3, y4 is Point of (TOP-REAL n) : ( y3 in X & y4 in B ) } & x in { (y3 + y4) where y3, y4 is Point of (TOP-REAL n) : ( y3 in Y & y4 in B ) } ) by A1;
hence x in (X (+) B) /\ (Y (+) B) by XBOOLE_0:def 4; :: thesis: verum