theorem :: TAXONOM2:13

for Y being set
for H being covering Hierarchy of Y st H is with_max's holds
ex P being a_partition of Y st P c= H