:: deftheorem Def12 defines GenUnivAlg UNIALG_2:def 12 :
for U0 being Universal_Algebra
for A being Subset of U0 st ( Constants U0 <> {} or A <> {} ) holds
for b₃ being strict SubAlgebra of U0 holds
( b₃ = GenUnivAlg A iff ( A c= the carrier of b₃ & ( for U1 being SubAlgebra of U0 st A c= the carrier of U1 holds
b₃ is SubAlgebra of U1 ) ) );