:: deftheorem Def14 defines B_SUP BVFUNC_1:def 14 :
for Y being non empty set
for a being Function of Y,BOOLEAN holds
( ( ( for x being Element of Y holds a . x = FALSE ) implies B_SUP a = O_el Y ) & ( not for x being Element of Y holds a . x = FALSE implies B_SUP a = I_el Y ) );