theorem Th54: :: GLIBPRE1:53

for G2 being _Graph
for v, e, w being object
for G1 being addAdjVertex of G2,v,e,w holds
( the_Vertices_of G1 c= (the_Vertices_of G2) \/ {v,w} & the_Edges_of G1 c= (the_Edges_of G2) \/ {e} )