:: deftheorem Def1 defines SubAlgebra-Family UNIALG_3:def 1 :
for U0 being Universal_Algebra
for b₂ being set holds
( b₂ is SubAlgebra-Family of U0 iff for U1 being set st U1 in b₂ holds
U1 is SubAlgebra of U0 );