:: deftheorem Def4 defines opers_closed POLYALG1:def 4 :
for L being non empty multMagma
for B being non empty AlgebraStr over L
for A being Subset of B holds
( A is opers_closed iff ( A is linearly-closed & ( for x, y being Element of B st x in A & y in A holds
x * y in A ) & 1. B in A & 0. B in A ) );