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