theorem Th72: :: GLIB_006:68

for G2 being _Graph
for G1 being Supergraph of G2
for v being Vertex of G2 holds v is Vertex of G1 by Th71;