let G1 be _Graph; :: thesis: for v being object
for G2 being addVertex of G1,v
for G3 being GraphComplement of G1 st not v in the_Vertices_of G1 holds
ex G4 being addAdjVertexAll of G3,v st G4 is GraphComplement of G2
let v be object ; :: thesis: for G2 being addVertex of G1,v
for G3 being GraphComplement of G1 st not v in the_Vertices_of G1 holds
ex G4 being addAdjVertexAll of G3,v st G4 is GraphComplement of G2
let G2 be addVertex of G1,v; :: thesis: for G3 being GraphComplement of G1 st not v in the_Vertices_of G1 holds
ex G4 being addAdjVertexAll of G3,v st G4 is GraphComplement of G2
let G3 be GraphComplement of G1; :: thesis: ( not v in the_Vertices_of G1 implies ex G4 being addAdjVertexAll of G3,v st G4 is GraphComplement of G2 )
assume A1: not v in the_Vertices_of G1 ; :: thesis: ex G4 being addAdjVertexAll of G3,v st G4 is GraphComplement of G2
the_Edges_of G1 misses the_Edges_of G3 by Th98;
then A2: the_Edges_of G2 misses the_Edges_of G3 by GLIB_006:def 10;
( {} is Subset of (the_Vertices_of G1) & G2 is addAdjVertexAll of G1,v, {} ) by XBOOLE_1:2, GLIBPRE0:51;
then consider G4 being addAdjVertexAll of G3,v,(the_Vertices_of G1) \ {} such that
A3: G4 is GraphComplement of G2 by A1, A2, Th105;
reconsider G4 = G4 as addAdjVertexAll of G3,v by Th98;
take G4 ; :: thesis: G4 is GraphComplement of G2
thus G4 is GraphComplement of G2 by A3; :: thesis: verum