let G be void SimpleGraph; :: thesis: clique# G = 0
assume A: clique# G <> 0 ; :: thesis: contradiction
consider C being finite Clique of G such that
B: order C = clique# G by Lcliqueno;
Vertices C c= Vertices G by ZFMISC_1:77;
hence contradiction by A, B; :: thesis: verum