theorem :: MATHMORP:53

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B being Subset of T holds (X (o) B) (o) B = X (o) B by Th50;