let R be RelStr ; :: thesis: 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
let A be finite StableSet of R; :: thesis: for n being Nat st n <= card A holds
ex B being finite StableSet of R st card B = n
let n be Nat; :: thesis: ( n <= card A implies ex B being finite StableSet of R st card B = n )
assume A: n <= card A ; :: thesis: ex B being finite StableSet of R st card B = n
consider BB being finite Subset of A such that
B: card BB = n by A, FINSEQ_4:87;
reconsider BB = BB as finite StableSet of R by AChain0;
take BB ; :: thesis: card BB = n
thus card BB = n by B; :: thesis: verum