theorem Th49: :: DILWORTH:49

for R being non empty transitive antisymmetric with_finite_stability# RelStr
for A being StableSet of R
for U being Clique-partition of (subrelstr (Upper A))
for L being Clique-partition of (subrelstr (Lower A)) st card A = stability# R & card U = stability# R & card L = stability# R holds
ex C being Clique-partition of R st card C = stability# R