:: deftheorem Def11 defines I_el BVFUNC_1:def 11 :
for Y being non empty set
for b₂ being Function of Y,BOOLEAN holds
( b₂ = I_el Y iff for x being Element of Y holds b₂ . x = TRUE );