let G1 be _Graph; :: thesis: for v being set
for G2 being removeVertex of G1,v st ( G1 is _trivial or not v in the_Vertices_of G1 ) holds
G1 == G2
let v be set ; :: thesis: for G2 being removeVertex of G1,v st ( G1 is _trivial or not v in the_Vertices_of G1 ) holds
G1 == G2
let G2 be removeVertex of G1,v; :: thesis: ( ( G1 is _trivial or not v in the_Vertices_of G1 ) implies G1 == G2 )
assume ( G1 is _trivial or not v in the_Vertices_of G1 ) ; :: thesis: G1 == G2

per cases then ( G1 is _trivial or not v in the_Vertices_of G1 ) ;

suppose G1 is _trivial ; :: thesis: G1 == G2

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

per cases ( ( (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}) ) 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: G1 == G2

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

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: G1 == G2

hence G1 == G2 by Def37; :: thesis: verum

end;

end;

end;

suppose not v in the_Vertices_of G1 ; :: thesis: G1 == G2

hence G1 == G2 by Lm10; :: thesis: verum

end;

end;