theorem Th115: :: GLIB_000:115

for G1, G2 being _Graph
for v being set st G1 == G2 & ( G1 is _trivial or not v in the_Vertices_of G1 ) holds
G2 is removeVertex of G1,v