let G1 be _Graph; for v being object
for G2 being addAdjVertexAll of G1,v
for G3 being GraphComplement of G1
for G4 being addVertex of G3,v st not v in the_Vertices_of G1 & the_Edges_of G2 misses the_Edges_of G3 holds
G4 is GraphComplement of G2
let v be object ; for G2 being addAdjVertexAll of G1,v
for G3 being GraphComplement of G1
for G4 being addVertex of G3,v st not v in the_Vertices_of G1 & the_Edges_of G2 misses the_Edges_of G3 holds
G4 is GraphComplement of G2
let G2 be addAdjVertexAll of G1,v; for G3 being GraphComplement of G1
for G4 being addVertex of G3,v st not v in the_Vertices_of G1 & the_Edges_of G2 misses the_Edges_of G3 holds
G4 is GraphComplement of G2
let G3 be GraphComplement of G1; for G4 being addVertex of G3,v st not v in the_Vertices_of G1 & the_Edges_of G2 misses the_Edges_of G3 holds
G4 is GraphComplement of G2
let G4 be addVertex of G3,v; ( not v in the_Vertices_of G1 & the_Edges_of G2 misses the_Edges_of G3 implies G4 is GraphComplement of G2 )
assume A1:
( not v in the_Vertices_of G1 & the_Edges_of G2 misses the_Edges_of G3 )
; G4 is GraphComplement of G2
the_Vertices_of G1 c= the_Vertices_of G1
;
then consider G9 being addAdjVertexAll of G3,v,(the_Vertices_of G1) \ (the_Vertices_of G1) such that
A2:
G9 is GraphComplement of G2
by A1, Th105;
(the_Vertices_of G1) \ (the_Vertices_of G1) = {}
by XBOOLE_1:37;
then
G9 is addVertex of G3,v
by GLIB_007:55;
then
G4 == G9
by GLIB_006:77;
hence
G4 is GraphComplement of G2
by A2, Th97; verum