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

now :: thesis: for a being object 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 object ; :: 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 A2: {a} in CompleteSGraph (Vertices G) by Th33;

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 Th13; :: thesis: verum

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: 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 A1, Th24;
then a in Vertices (CompleteSGraph (Vertices G)) by Th24;
hence a in Vertices G by Lm1; :: thesis: verum

end;

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