:: deftheorem Def14 defines Sub UNIALG_2:def 14 :
for U0 being Universal_Algebra
for b₂ being set holds
( b₂ = Sub U0 iff for x being object holds
( x in b₂ iff x is strict SubAlgebra of U0 ) );