:: deftheorem defines is_a_dependent_set_of PARTIT1:def 1 :
for Y being non empty set
for PA being a_partition of Y
for b being set holds
( b is_a_dependent_set_of PA iff ex B being set st
( B c= PA & B <> {} & b = union B ) );