theorem Th17: :: TAXONOM2:18

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