theorem Th55: :: GLIB_007:55

for G2 being _Graph
for v being object
for G1 being addAdjVertexAll of G2,v, {} holds G1 is addVertex of G2,v