for G1 being _finite _Graph
for G2 being Subgraph of G1 st G1 .size() = G2 .size() holds
G1 is addVertices of G2,(the_Vertices_of G1) \ (the_Vertices_of G2)