let X be finite set ; :: thesis: clique# (CompleteSGraph X) = card X
set G = CompleteSGraph X;
A1: order (CompleteSGraph X) = card X by Lm1;
A2: 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 A1, A2, Def15; :: thesis: verum