for G1 being _Graph
for G2 being Subgraph of G1 holds G2 is inducedSubgraph of G1, the_Vertices_of G2, the_Edges_of G2