take G = the void SimpleGraph; :: thesis: G is with_finite_clique#
{} in G by Th20;
then {{}} c= G by ZFMISC_1:31;
then reconsider C = {{}} as finite Clique of G by Th48;
take C ; :: according to SCMYCIEL:def 14 :: thesis: for D being finite Clique of G holds order D <= order C
let D be finite Clique of G; :: thesis: order D <= order C
union D c= union G by ZFMISC_1:77;
hence order D <= order C ; :: thesis: verum