let n be Element of NAT ; :: thesis: for B, C being Subset of (TOP-REAL n)
for y being Point of (TOP-REAL n) holds (B /\ C) + y = (B + y) /\ (C + y)
let B, C be Subset of (TOP-REAL n); :: thesis: for y being Point of (TOP-REAL n) holds (B /\ C) + y = (B + y) /\ (C + y)
let y be Point of (TOP-REAL n); :: thesis: (B /\ C) + y = (B + y) /\ (C + y)
thus (B /\ C) + y c= (B + y) /\ (C + y) :: according to XBOOLE_0:def 10 :: thesis: (B + y) /\ (C + y) c= (B /\ C) + y

proof

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

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (B + y) /\ (C + y) or x in (B /\ C) + y )
assume x in (B + y) /\ (C + y) ; :: thesis: x in (B /\ C) + y
then A2: ( x in B + y & x in C + y ) by XBOOLE_0:def 4;
then consider y3 being Point of (TOP-REAL n) such that
A3: ( x = y3 + y & y3 in B ) ;
consider y2 being Point of (TOP-REAL n) such that
A4: ( x = y2 + y & y2 in C ) by A2;
(y2 + y) - y = y3 by A3, A4, EUCLID:52;
then A5: y2 = y3 by EUCLID:52;
then y2 in B /\ C by A3, A4, XBOOLE_0:def 4;
hence x in (B /\ C) + y by A3, A5; :: thesis: verum