theorem Th22: :: POLYALG1:22

for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for A being non empty Subset of (Formal-Series L) st A = the carrier of (Polynom-Ring L) holds
A is opers_closed