:: deftheorem defines CompF BVFUNC_2:def 7 :
for Y being non empty set
for PA being a_partition of Y
for G being Subset of (PARTITIONS Y) holds CompF (PA,G) = '/\' (G \ {PA});