:: deftheorem defines is_min_depend PARTIT1:def 2 :
for Y being non empty set
for PA, PB being a_partition of Y
for b being set holds
( b is_min_depend PA,PB iff ( b is_a_dependent_set_of PA & b is_a_dependent_set_of PB & ( for d being set st d c= b & d is_a_dependent_set_of PA & d is_a_dependent_set_of PB holds
d = b ) ) );