:: deftheorem defines Ex BVFUNC_2:def 10 :
for Y being non empty set
for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y holds Ex (a,PA,G) = B_SUP (a,(CompF (PA,G)));