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

end;

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