let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; :: thesis: for X, Y, B being Subset of T holds B (+) (X /\ Y) c= (B (+) X) /\ (B (+) Y)
let X, Y, B be Subset of T; :: thesis: B (+) (X /\ Y) c= (B (+) X) /\ (B (+) Y)
B (+) (X /\ Y) = (X /\ Y) (+) B by Th12;
then B (+) (X /\ Y) c= (X (+) B) /\ (Y (+) B) by Th34;
then B (+) (X /\ Y) c= (B (+) X) /\ (Y (+) B) by Th12;
hence B (+) (X /\ Y) c= (B (+) X) /\ (B (+) Y) by Th12; :: thesis: verum