theorem Th18: :: TAXONOM2:19

for X, h being non empty set st h c= X holds
for Pmax being a_partition of X st ex hy being set st
( hy in Pmax & hy c= h ) & ( for x being set holds
( not x in Pmax or x c= h or h c= x or h misses x ) ) holds
for Pb being set st ( for x being set holds
( x in Pb iff ( x in Pmax & x misses h ) ) ) holds
( Pb \/ {h} is a_partition of X & Pmax is_finer_than Pb \/ {h} & ( for Pmin being a_partition of X st Pmax is_finer_than Pmin holds
for hw being set st hw in Pmin & h c= hw holds
Pb \/ {h} is_finer_than Pmin ) )