for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y, B being Subset of T holds B (+) (X /\ Y) c= (B (+) X) /\ (B (+) Y)