:: deftheorem defines is_upper_min_depend_of BVFUNC_2:def 2 :
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for b being set holds
( b is_upper_min_depend_of G iff ( ( for d being a_partition of Y st d in G holds
b is_a_dependent_set_of d ) & ( for e being set st e c= b & ( for d being a_partition of Y st d in G holds
e is_a_dependent_set_of d ) holds
e = b ) ) );