let G, CG be SimpleGraph; :: thesis: ( CG = (CompleteSGraph (Vertices G)) \ (Edges G) implies (CompleteSGraph (Vertices CG)) \ (Edges CG) = G )
assume AAa: CG = (CompleteSGraph (Vertices G)) \ (Edges G) ; :: thesis: (CompleteSGraph (Vertices CG)) \ (Edges CG) = G
set CCG = (CompleteSGraph (Vertices CG)) \ (Edges CG);
A: Vertices G = Vertices CG by AAa, Compl1;
Aa: Vertices CG = Vertices ((CompleteSGraph (Vertices CG)) \ (Edges CG)) by Compl1;
(CompleteSGraph (Vertices CG)) \ (Edges CG) is SimpleGraph by CisSG;
then B: (CompleteSGraph (Vertices CG)) \ (Edges CG) = ({{}} \/ (singletons (Vertices ((CompleteSGraph (Vertices CG)) \ (Edges CG))))) \/ (Edges ((CompleteSGraph (Vertices CG)) \ (Edges CG))) by SG0;
D: G = ({{}} \/ (singletons (Vertices G))) \/ (Edges G) by SG0;

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

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

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

assume S1: a in Edges ((CompleteSGraph (Vertices CG)) \ (Edges CG)) ; :: thesis: a in Edges G
then consider x, y being set such that
A0: x <> y and
A1: ( x in Vertices ((CompleteSGraph (Vertices CG)) \ (Edges CG)) & y in Vertices ((CompleteSGraph (Vertices CG)) \ (Edges CG)) ) and
B1: a = {x,y} by SG4;
{x,y} nin Edges CG by A0, Aa, S1, B1, A1, Compl1a;
hence a in Edges G by A0, Aa, A, A1, B1, AAa, Compl1a; :: thesis: verum

end;

assume S1: a in Edges G ; :: thesis: a in Edges ((CompleteSGraph (Vertices CG)) \ (Edges CG))
then consider x, y being set such that
A0: x <> y and
A1: ( x in Vertices G & y in Vertices G ) and
B1: a = {x,y} by SG4;
{x,y} nin Edges CG by A0, S1, B1, A1, AAa, Compl1a;
hence a in Edges ((CompleteSGraph (Vertices CG)) \ (Edges CG)) by A0, A, A1, B1, Compl1a; :: thesis: verum

end;

hence (CompleteSGraph (Vertices CG)) \ (Edges CG) = G by A, Aa, B, D, TARSKI:1; :: thesis: verum