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

proof

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 y being Point of (TOP-REAL n) such that
A1: ( x = y & B + y c= X /\ Y ) ;
( B + y c= X & B + y c= Y ) by A1, XBOOLE_1:18;
then ( x in { y1 where y1 is Point of (TOP-REAL n) : B + y1 c= X } & x in { y1 where y1 is Point of (TOP-REAL n) : B + y1 c= Y } ) by A1;
hence x in (X (-) B) /\ (Y (-) B) by XBOOLE_0:def 4; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (X (-) B) /\ (Y (-) B) or x in (X /\ Y) (-) B )
assume x in (X (-) B) /\ (Y (-) B) ; :: thesis: x in (X /\ Y) (-) B
then A2: ( x in X (-) B & x in Y (-) B ) by XBOOLE_0:def 4;
then consider y being Point of (TOP-REAL n) such that
A3: ( x = y & B + y c= X ) ;
consider y2 being Point of (TOP-REAL n) such that
A4: ( x = y2 & B + y2 c= Y ) by A2;
B + y c= X /\ Y

proof

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

end;

hence x in (X /\ Y) (-) B by A3; :: thesis: verum