theorem Th6: :: PARTIT1:6

for Y being non empty set
for PA, PB being a_partition of Y st PA '>' PB holds
for b being set st b in PA holds
b is_a_dependent_set_of PB