{} in G by Th20;
then reconsider C = {{}} as Subgraph of G by ZFMISC_1:31;
C is clique by Th48;
hence ex b₁ being Clique of G st b₁ is finite ; :: thesis: verum