let X be finite set ; :: thesis: clique# (CompleteSGraph X) = card X
set G = CompleteSGraph X;
B: order (CompleteSGraph X) = card X by CSGLem1;
C: CompleteSGraph X c= CompleteSGraph X ;
for T being finite Clique of (CompleteSGraph X) holds order T <= order (CompleteSGraph X) by NAT_1:43, ZFMISC_1:77;
hence clique# (CompleteSGraph X) = card X by B, C, Lcliqueno; :: thesis: verum