theorem Th7: :: PARTIT1:7

for Y being non empty set
for PA being a_partition of Y holds Y is_a_dependent_set_of PA