let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; :: thesis: for X, Y, B being Subset of T holds (X /\ Y) (-) B = (X (-) B) /\ (Y (-) B)
let X, Y, B be Subset of T; :: 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 object ; :: 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 T such that
A1: x = y and
A2: B + y c= X /\ Y ;
B + y c= Y by A2, XBOOLE_1:18;
then A3: x in { y1 where y1 is Point of T : B + y1 c= Y } by A1;
B + y c= X by A2, XBOOLE_1:18;
then x in { y1 where y1 is Point of T : B + y1 c= X } by A1;
hence x in (X (-) B) /\ (Y (-) B) by A3, XBOOLE_0:def 4; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (X (-) B) /\ (Y (-) B) or x in (X /\ Y) (-) B )
assume A4: x in (X (-) B) /\ (Y (-) B) ; :: thesis: x in (X /\ Y) (-) B
then x in X (-) B by XBOOLE_0:def 4;
then consider y being Point of T such that
A5: x = y and
A6: B + y c= X ;
x in Y (-) B by A4, XBOOLE_0:def 4;
then A7: ex y2 being Point of T st
( x = y2 & B + y2 c= Y ) ;
B + y c= X /\ Y by A5, A6, A7, XBOOLE_0:def 4;
hence x in (X /\ Y) (-) B by A5; :: thesis: verum