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

now :: thesis: for a being set holds
( ( a in Vertices G implies a in Vertices ((CompleteSGraph (Vertices G)) \ (Edges G)) ) & ( a in Vertices ((CompleteSGraph (Vertices G)) \ (Edges G)) implies a in Vertices G ) )

let a be set ; :: thesis: ( ( a in Vertices G implies a in Vertices ((CompleteSGraph (Vertices G)) \ (Edges G)) ) & ( a in Vertices ((CompleteSGraph (Vertices G)) \ (Edges G)) implies a in Vertices G ) )

hereby :: thesis: ( a in Vertices ((CompleteSGraph (Vertices G)) \ (Edges G)) implies a in Vertices G )

assume a in Vertices G ; :: thesis: a in Vertices ((CompleteSGraph (Vertices G)) \ (Edges G))
then A1: {a} in CompleteSGraph (Vertices G) by CSG1a;

now :: thesis: not {a} in Edges G

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

end;

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

end;

assume a in Vertices ((CompleteSGraph (Vertices G)) \ (Edges G)) ; :: thesis: a in Vertices G
then {a} in (CompleteSGraph (Vertices G)) \ (Edges G) by Aa, Vertices0;
then a in Vertices (CompleteSGraph (Vertices G)) by Vertices0;
hence a in Vertices G by CSGLem1; :: thesis: verum

end;

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