let R be RelStr ; :: thesis: for C being finite Clique of R
for n being Nat st n <= card C holds
ex B being finite Clique of R st card B = n
let C be finite Clique of R; :: thesis: for n being Nat st n <= card C holds
ex B being finite Clique of R st card B = n
let n be Nat; :: thesis: ( n <= card C implies ex B being finite Clique of R st card B = n )
assume A: n <= card C ; :: thesis: ex B being finite Clique of R st card B = n
consider BB being finite Subset of C such that
B: card BB = n by A, FINSEQ_4:87;
reconsider BB = BB as finite Clique of R by Clique37;
take BB ; :: thesis: card BB = n
thus card BB = n by B; :: thesis: verum