let G, CG be SimpleGraph; :: thesis: ( CG = (CompleteSGraph (Vertices G)) \ (Edges G) implies (CompleteSGraph (Vertices CG)) \ (Edges CG) = G )
assume A1: CG = (CompleteSGraph (Vertices G)) \ (Edges G) ; :: thesis: (CompleteSGraph (Vertices CG)) \ (Edges CG) = G
set CCG = (CompleteSGraph (Vertices CG)) \ (Edges CG);
A2: Vertices G = Vertices CG by A1, Lm4;
A3: Vertices CG = Vertices ((CompleteSGraph (Vertices CG)) \ (Edges CG)) by Lm4;
(CompleteSGraph (Vertices CG)) \ (Edges CG) is SimpleGraph by Lm3;
then A4: (CompleteSGraph (Vertices CG)) \ (Edges CG) = ({{}} \/ (singletons (Vertices ((CompleteSGraph (Vertices CG)) \ (Edges CG))))) \/ (Edges ((CompleteSGraph (Vertices CG)) \ (Edges CG))) by Th27;
A5: G = ({{}} \/ (singletons (Vertices G))) \/ (Edges G) by Th27;
now :: thesis: for a being object 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 object ; :: 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 A6: a in Edges ((CompleteSGraph (Vertices CG)) \ (Edges CG)) ; :: thesis: a in Edges G
then consider x, y being set such that
A7: x <> y and
A8: ( x in Vertices ((CompleteSGraph (Vertices CG)) \ (Edges CG)) & y in Vertices ((CompleteSGraph (Vertices CG)) \ (Edges CG)) ) and
A9: a = {x,y} by Th11;
{x,y} nin Edges CG by A7, A3, A6, A9, A8, Lm5;
hence a in Edges G by A7, A3, A2, A8, A9, A1, Lm5; :: thesis: verum
end;
assume A10: a in Edges G ; :: thesis: a in Edges ((CompleteSGraph (Vertices CG)) \ (Edges CG))
then consider x, y being set such that
A11: x <> y and
A12: ( x in Vertices G & y in Vertices G ) and
A13: a = {x,y} by Th11;
{x,y} nin Edges CG by A11, A10, A13, A12, A1, Lm5;
hence a in Edges ((CompleteSGraph (Vertices CG)) \ (Edges CG)) by A11, A2, A12, A13, Lm5; :: thesis: verum
end;
hence (CompleteSGraph (Vertices CG)) \ (Edges CG) = G by A2, A3, A4, A5, TARSKI:2; :: thesis: verum