theorem :: MATHMORP:30

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