let G be SimpleGraph; :: thesis:
set CG = (CompleteSGraph (Vertices G)) \ (Edges G);
A1: (CompleteSGraph (Vertices G)) \ (Edges G) is SimpleGraph by Lm3;

let a be object ; :: thesis:

hereby :: thesis:

assume a in Vertices G ; :: thesis:
then A2: {a} in CompleteSGraph (Vertices G) by Th33;

assume {a} in Edges G ; :: thesis:
then {a,a} in Edges G by ENUMSET1:29;
hence contradiction by Th13; :: thesis:

end;

then {a} in (CompleteSGraph (Vertices G)) \ (Edges G) by A2, XBOOLE_0:def 5;
hence a in Vertices ((CompleteSGraph (Vertices G)) \ (Edges G)) by A1, Th24; :: thesis:

end;

assume a in Vertices ((CompleteSGraph (Vertices G)) \ (Edges G)) ; :: thesis:
then {a} in (CompleteSGraph (Vertices G)) \ (Edges G) by A1, Th24;
then a in Vertices (CompleteSGraph (Vertices G)) by Th24;
hence a in Vertices G by Lm1; :: thesis:

end;

hence Vertices G = Vertices ((CompleteSGraph (Vertices G)) \ (Edges G)) by TARSKI:2; :: thesis: