:: deftheorem defines generating BVFUNC_2:def 4 :
for Y being non empty set
for G being Subset of (PARTITIONS Y) holds
( G is generating iff '/\' G = %I Y );