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 c= (X (+) B) /\ (Y (+) B)
let X, Y, B be Subset of T; :: thesis: (X /\ Y) (+) B c= (X (+) B) /\ (Y (+) B)
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 y1, y2 being Point of T such that
A1: x = y1 + y2 and
A2: y1 in X /\ Y and
A3: y2 in B ;
y1 in Y by A2, XBOOLE_0:def 4;
then A4: x in { (y3 + y4) where y3, y4 is Point of T : ( y3 in Y & y4 in B ) } by A1, A3;
y1 in X by A2, XBOOLE_0:def 4;
then x in { (y3 + y4) where y3, y4 is Point of T : ( y3 in X & y4 in B ) } by A1, A3;
hence x in (X (+) B) /\ (Y (+) B) by A4, XBOOLE_0:def 4; :: thesis: verum