theorem Th47: :: GLIB_008:47

for G1 being non _trivial simple _Graph
for v being Vertex of G1
for G2 being removeVertex of G1,v holds G1 is addAdjVertexAll of G2,v,v .allNeighbors()