theorem :: GLIB_008:35

for G1 being non _trivial _Graph
for v being Vertex of G1
for G2 being removeVertex of G1,v st v is isolated holds
G1 is addVertex of G2,v