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