:: deftheorem Def3 defines Carr UNIALG_3:def 3 :
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 holds b₂ . u = carr u );