:: deftheorem Def17 defines B_SUP BVFUNC_1:def 17 :
for Y being non empty set
for a being Function of Y,BOOLEAN
for PA being a_partition of Y
for b₄ being Function of Y,BOOLEAN holds
( b₄ = B_SUP (a,PA) iff for y being Element of Y holds
( ( ex x being Element of Y st
( x in EqClass (y,PA) & a . x = TRUE ) implies b₄ . y = TRUE ) & ( ( for x being Element of Y holds
( not x in EqClass (y,PA) or not a . x = TRUE ) ) implies b₄ . y = FALSE ) ) );