for G1 being edgeless _Graph
for G2 being Subgraph of G1 holds G1 is addVertices of G2,(the_Vertices_of G1) \ (the_Vertices_of G2)