let G be SimpleGraph; :: thesis: ( G is finite implies G is with_finite_clique# )
assume G is finite ; :: thesis: G is with_finite_clique#
then reconsider R9 = G as finite SimpleGraph ;
defpred S₁[ Nat] means ex c being finite Clique of G st order c = c₁;
A1: for k being Nat st S₁[k] holds
k <= card R9

proof

let k be Nat; :: thesis: ( S₁[k] implies k <= card R9 )
assume S₁[k] ; :: thesis: k <= card R9
then consider c being finite Clique of G such that
A2: order c = k ;
A3: card c <= card R9 by NAT_1:43;
order c <= card c by Th26;
hence k <= card R9 by A2, A3, XXREAL_0:2; :: thesis: verum

end;

{} in G by Th20;
then {{}} c= G by ZFMISC_1:31;
then reconsider E = {{}} as finite Clique of G by Th48;
order E = 0 ;
then A4: ex k being Nat st S₁[k] ;
consider k being Nat such that
A5: S₁[k] and
A6: for n being Nat st S₁[n] holds
n <= k from NAT_1:sch 6(A1, A4);
consider c being finite Clique of G such that
A7: order c = k by A5;
for D being finite Clique of G holds order D <= order c by A7, A6;
hence G is with_finite_clique# ; :: thesis: verum