theorem Th33: :: GLIB_008:33

for G2 being _Graph
for G1 being Supergraph of G2 st the_Edges_of G1 = the_Edges_of G2 holds
G1 is addVertices of G2,(the_Vertices_of G1) \ (the_Vertices_of G2)