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 {} 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