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 and
A2: y2 in B \/ C ;
( y2 in B or y2 in C ) by A2, XBOOLE_0:def 3;
then ( x in { (y1 + y) where y1 is Point of (TOP-REAL n) : y1 in B } or 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 3; :: 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 ( x in B + y or x in C + y ) by XBOOLE_0:def 3;
then consider y2 being Point of (TOP-REAL n) such that
A3: ( ( x = y2 + y & y2 in B ) or ( x = y2 + y & y2 in C ) ) ;
y2 in B \/ C by A3, XBOOLE_0:def 3;
hence x in (B \/ C) + y by A3; :: thesis: verum