theorem Th10: :: PARTIT1:10

for Y being non empty set
for PA being a_partition of Y
for X being Subset of Y st X is_a_dependent_set_of PA & X <> Y holds
X ` is_a_dependent_set_of PA