let G1 be _Graph; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: verum