let G1 be _Graph; :: thesis: for V being proper Subset of (the_Vertices_of G1)
for G2 being removeVertices of G1,V
for G3 being GraphComplement of G1
for G4 being removeVertices of G3,V holds G4 is GraphComplement of G2
let V be proper Subset of (the_Vertices_of G1); :: thesis: for G2 being removeVertices of G1,V
for G3 being GraphComplement of G1
for G4 being removeVertices of G3,V holds G4 is GraphComplement of G2
let G2 be removeVertices of G1,V; :: thesis: for G3 being GraphComplement of G1
for G4 being removeVertices of G3,V holds G4 is GraphComplement of G2
let G3 be GraphComplement of G1; :: thesis: for G4 being removeVertices of G3,V holds G4 is GraphComplement of G2
let G4 be removeVertices of G3,V; :: thesis: G4 is GraphComplement of G2
( (the_Vertices_of G1) \ V is non empty Subset of (the_Vertices_of G1) & (the_Vertices_of G1) \ V = (the_Vertices_of G3) \ V ) by Th98, XBOOLE_1:105, GLIBPRE0:6;
hence G4 is GraphComplement of G2 by Th108; :: thesis: verum