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 A1: n <= card A ; :: thesis: ex B being finite StableSet of R st card B = n
consider BB being finite Subset of A such that
A2: card BB = n by A1, FINSEQ_4:72;
reconsider BB = BB as finite StableSet of R by Th16;
take BB ; :: thesis: card BB = n
thus card BB = n by A2; :: thesis: verum