let X be set ; :: thesis: CompleteSGraph X is clique
CompleteSGraph X = CompleteSGraph (Vertices (CompleteSGraph X)) by CSGLem1;
hence CompleteSGraph X is clique by Lclique; :: thesis: verum