:: deftheorem Def2 defines carr UNIALG_3:def 2 :
for U0 being Universal_Algebra
for u being Element of Sub U0
for b₃ being Subset of U0 holds
( b₃ = carr u iff ex U1 being SubAlgebra of U0 st
( u = U1 & b₃ = the carrier of U1 ) );