for L being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
for S being Subset of L st 0. L in S holds
for a being Element of L holds S c= S + (a * S)