theorem :: DILWORTH:53

for R being transitive antisymmetric with_finite_stability# RelStr ex C being Clique-partition of R st card C = stability# R