theorem :: GLIB_012:70
for G1 being _Graph
for V being proper Subset of (the_Vertices_of G1)
for G2 being removeVertices of G1,V
for G3 being LGraphComplement of G1
for G4 being removeVertices of G3,V holds G4 is LGraphComplement of G2