let G1, G2 be _Graph; :: thesis: for v being set st G1 == G2 & not v in the_Vertices_of G1 holds
G2 is removeVertex of G1,v
let v be set ; :: thesis: ( G1 == G2 & not v in the_Vertices_of G1 implies G2 is removeVertex of G1,v )
assume A1: ( G1 == G2 & not v in the_Vertices_of G1 ) ; :: thesis: G2 is removeVertex of G1,v
then A2: G2 is Subgraph of G1 by GLIB_000:87;
set V = (the_Vertices_of G1) \ {v};
A3: (the_Vertices_of G1) \ {v} = the_Vertices_of G1 by A1, ZFMISC_1:57;
A4: G1 .edgesBetween ((the_Vertices_of G1) \ {v}) = the_Edges_of G1 by A3, GLIB_000:34
.= the_Edges_of G2 by A1, GLIB_000:def 34 ;
(the_Vertices_of G1) \ {v} = the_Vertices_of G2 by A1, A3, GLIB_000:def 34;
hence G2 is removeVertex of G1,v by A2, A4, GLIB_000:def 37; :: thesis: verum