:: deftheorem Def8 defines UniAlgSetClosed UNIALG_2:def 8 :
for U0 being Universal_Algebra
for A being non empty Subset of U0 st A is opers_closed holds
UniAlgSetClosed A = UAStr(# A,(Opers (U0,A)) #);