theorem :: TAXONOM2:20

for X being non empty set
for H being covering T_3 Hierarchy of X st H is lower-bounded & not {} in H & ( for C1 being set st C1 <> {} & C1 c= PARTITIONS X & ( for P1, P2 being set st P1 in C1 & P2 in C1 & not P1 is_finer_than P2 holds
P2 is_finer_than P1 ) holds
ex PX, PY being set st
( PX in C1 & PY in C1 & ( for PZ being set st PZ in C1 holds
( PZ is_finer_than PY & PX is_finer_than PZ ) ) ) ) holds
ex C being Classification of X st union C = H