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
( B c= C & 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
( B c= C & card B = n )
let n be Nat; :: thesis: ( n <= card C implies ex B being finite Clique of R st
( B c= C & card B = n ) )
assume A1: n <= card C ; :: thesis: ex B being finite Clique of R st
( B c= C & card B = n )
consider BB being finite Subset of C such that
A2: card BB = n by A1, FINSEQ_4:72;
reconsider BB = BB as finite Clique of R by Th9;
take BB ; :: thesis: ( BB c= C & card BB = n )
thus ( BB c= C & card BB = n ) by A2; :: thesis: verum