theorem Th12: :: MATHMORP:12
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y being Subset of T holds X (+) Y = Y (+) X