theorem Th17: :: DILWORTH:17

for R being RelStr
for A being finite StableSet of R
for n being Nat st n <= card A holds
ex B being finite StableSet of R st card B = n