let G1 be _Graph; :: thesis: for v being set
for G2 being removeVertex of G1,v st not v in the_Vertices_of G1 holds
G1 == G2
let v be set ; :: thesis: for G2 being removeVertex of G1,v st not v in the_Vertices_of G1 holds
G1 == G2
let G2 be removeVertex of G1,v; :: thesis: ( not v in the_Vertices_of G1 implies G1 == G2 )
set V = (the_Vertices_of G1) \ {v};
assume not v in the_Vertices_of G1 ; :: thesis: G1 == G2
then A1: (the_Vertices_of G1) \ {v} = the_Vertices_of G1 by ZFMISC_1:57;
then ( the_Vertices_of G2 = (the_Vertices_of G1) \ {v} & the_Edges_of G2 = G1 .edgesBetween ((the_Vertices_of G1) \ {v}) ) by Def37;
then A2: ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = the_Edges_of G1 ) by A1, Th34;
G1 is Subgraph of G1 by Lm3;
hence G1 == G2 by A2, Th86; :: thesis: verum