theorem :: MATHMORP:56

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X being Subset of T st X = {} holds
0 (.) X = {}