:: deftheorem Def7 defines SubAlgebra UNIALG_2:def 7 :
for U0, b₂ being Universal_Algebra holds
( b₂ is SubAlgebra of U0 iff ( the carrier of b₂ is Subset of U0 & ( for B being non empty Subset of U0 st B = the carrier of b₂ holds
( the charact of b₂ = Opers (U0,B) & B is opers_closed ) ) ) );