theorem Th8: :: PARTIT1:8

for Y being non empty set
for PA being a_partition of Y
for F being Subset-Family of Y st Intersect F <> {} & ( for X being set st X in F holds
X is_a_dependent_set_of PA ) holds
Intersect F is_a_dependent_set_of PA