:: deftheorem Def15 defines | MSUALG_2:def 15 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A being MSSubset of U0 st A is opers_closed holds
U0 | A = MSAlgebra(# A,(Opers (U0,A)) #);