let G2 be _Graph; :: thesis: for v, V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
G2 is removeVertex of G1,v
let v, V be set ; :: thesis: for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
G2 is removeVertex of G1,v
let G1 be addAdjVertexAll of G2,v,V; :: thesis: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 implies G2 is removeVertex of G1,v )
assume A1: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 ) ; :: thesis: G2 is removeVertex of G1,v
A2: G2 is Subgraph of G1 by GLIB_006:57;
set V1 = (the_Vertices_of G1) \ {v};
the_Vertices_of G1 = (the_Vertices_of G2) \/ {v} by A1, Def4;
then A3: the_Vertices_of G2 = (the_Vertices_of G1) \ {v} by A1, ZFMISC_1:117;
then reconsider V1 = (the_Vertices_of G1) \ {v} as non empty Subset of (the_Vertices_of G1) ;
the_Edges_of G2 = G1 .edgesBetween V1 by A1, A3, Th53;
hence G2 is removeVertex of G1,v by A2, A3, GLIB_000:def 37; :: thesis: verum