:: deftheorem Def10 defines O_el BVFUNC_1:def 10 :
for Y being non empty set
for b₂ being Function of Y,BOOLEAN holds
( b₂ = O_el Y iff for x being Element of Y holds b₂ . x = FALSE );