:: deftheorem defines independent BVFUNC_2:def 5 :
for Y being non empty set
for G being Subset of (PARTITIONS Y) holds
( G is independent iff for h being Function
for F being Subset-Family of Y st dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) holds
Intersect F <> {} );