theorem :: TAXONOM2:15

for Y being set
for H being covering T_3 Hierarchy of Y st H is lower-bounded & not {} in H holds
for A being Subset of Y
for B being mutually-disjoint Subset-Family of Y st A in B & B c= H & ( for C being mutually-disjoint Subset-Family of Y st A in C & C c= H & union B c= union C holds
union B = union C ) holds
B is a_partition of Y