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 DLGraphComplement of G1
for G4 being removeVertices of G3,V holds G4 is DLGraphComplement of G2
let V be proper Subset of (the_Vertices_of G1); :: thesis: for G2 being removeVertices of G1,V
for G3 being DLGraphComplement of G1
for G4 being removeVertices of G3,V holds G4 is DLGraphComplement of G2
let G2 be removeVertices of G1,V; :: thesis: for G3 being DLGraphComplement of G1
for G4 being removeVertices of G3,V holds G4 is DLGraphComplement of G2
let G3 be DLGraphComplement of G1; :: thesis: for G4 being removeVertices of G3,V holds G4 is DLGraphComplement of G2
let G4 be removeVertices of G3,V; :: thesis: G4 is DLGraphComplement 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 Def6, XBOOLE_1:105, GLIBPRE0:6;
hence G4 is DLGraphComplement of G2 by Th52; :: thesis: verum