for G1 being _Graph
for G2 being Subgraph of G1
for x being set holds
( ( x in the_Vertices_of G2 implies x in the_Vertices_of G1 ) & ( x in the_Edges_of G2 implies x in the_Edges_of G1 ) ) ;