:: deftheorem defines ~ BASEL_2:def 2 :
for L being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr
for a being Element of the carrier of (Polynom-Ring L) holds ~ a = a;