:: deftheorem defines opers_closed UNIALG_2:def 4 :
for U0 being Universal_Algebra
for A being Subset of U0 holds
( A is opers_closed iff for o being operation of U0 holds A is_closed_on o );