theorem Th140: :: GLIB_006:136

for G2 being _Graph
for v1, e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2 holds G2 is inducedSubgraph of G1,(the_Vertices_of G2)