theorem Th48: :: DILWORTH:48

for R being finite RelStr
for A being StableSet of R
for C being Clique-partition of R st card C = card A holds
for c being set st c in C holds
ex a being Element of A st c /\ A = {a}