theorem Th71: :: GLIB_006:67

for G2 being _Graph
for G1 being Supergraph of G2
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 ) )