for Y being non empty set
for a being Function of Y,BOOLEAN
for PA being a_partition of Y st a is_dependent_of PA holds
PA is_finer_than GPart a