let G1 be _Graph; :: thesis:
let v be set ; :: thesis:
let G2 be removeVertex of G1,v; :: thesis:
assume ( G1 is _trivial or not v in the_Vertices_of G1 ) ; :: thesis:

suppose G1 is _trivial ; :: thesis:

then consider v1 being Vertex of G1 such that
A1: the_Vertices_of G1 = {v1} by GLIB_000:22;
set V = (the_Vertices_of G1) \ {v};
set E = G1 .edgesBetween ((the_Vertices_of G1) \ {v});

per cases ) \ {v} is non empty Subset of (the_Vertices_of G1) & G1 .edgesBetween ((the_Vertices_of G1) \ {v}) c= G1 .edgesBetween ((the_Vertices_of G1) \ {v}) ) or not (the_Vertices_of G1) \ {v} is non empty Subset of (the_Vertices_of G1) or not G1 .edgesBetween ((the_Vertices_of G1) \ {v}) c= G1 .edgesBetween ((the_Vertices_of G1) \ {v}) ) ;

suppose ( (the_Vertices_of G1) \ {v} is non empty Subset of (the_Vertices_of G1) & G1 .edgesBetween ((the_Vertices_of G1) \ {v}) c= G1 .edgesBetween ((the_Vertices_of G1) \ {v}) ) ; :: thesis:

then (the_Vertices_of G1) \ {v} = {v1} by A1, ZFMISC_1:33;
hence G1 == G2 by A1, Lm2, ZFMISC_1:57; :: thesis:

end;

suppose ( not (the_Vertices_of G1) \ {v} is non empty Subset of (the_Vertices_of G1) or not G1 .edgesBetween ((the_Vertices_of G1) \ {v}) c= G1 .edgesBetween ((the_Vertices_of G1) \ {v}) ) ; :: thesis:

hence G1 == G2 by GLIB_000:def 37; :: thesis:

end;

end;

end;

suppose not v in the_Vertices_of G1 ; :: thesis:

hence G1 == G2 by Lm2; :: thesis:

end;

end;