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

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (X + y) /\ (Y + y) or a in B )
assume A2: a in (X + y) /\ (Y + y) ; :: thesis: a in B
then A3: a in X + y by XBOOLE_0:def 4;
A4: a in Y + y by A2, XBOOLE_0:def 4;

per cases ( X + y c= B or Y + y c= B ) by A1;

suppose X + y c= B ; :: thesis: a in B

hence a in B by A3; :: thesis: verum

end;

suppose Y + y c= B ; :: thesis: a in B

hence a in B by A4; :: thesis: verum

end;

end;

end;

then (X /\ Y) + y c= B by Th28;
hence x in B (-) (X /\ Y) by A1; :: thesis: verum