:: deftheorem Def4 defines Carr UNIALG_3:def 4 :
for U0 being Universal_Algebra
for b₂ being Function of (Sub U0),(bool the carrier of U0) holds
( b₂ = Carr U0 iff for u being Element of Sub U0
for U1 being SubAlgebra of U0 st u = U1 holds
b₂ . u = the carrier of U1 );