let G1, G2 be _Graph; :: thesis: for v being set st G1 == G2 & ( G1 is _trivial or not v in the_Vertices_of G1 ) holds
G2 is removeVertex of G1,v
let v be set ; :: thesis: ( G1 == G2 & ( G1 is _trivial or not v in the_Vertices_of G1 ) implies G2 is removeVertex of G1,v )
assume that
A1: G1 == G2 and
A2: ( G1 is _trivial or not v in the_Vertices_of G1 ) ; :: thesis: G2 is removeVertex of G1,v
A3: G2 is Subgraph of G1 by A1, Th87;
set V = (the_Vertices_of G1) \ {v};

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

suppose G1 is _trivial ; :: thesis: G2 is removeVertex of G1,v

then consider v1 being Vertex of G1 such that
A4: the_Vertices_of G1 = {v1} by Th22;

per cases ( v = v1 or v <> v1 ) ;

suppose v = v1 ; :: thesis: G2 is removeVertex of G1,v

then (the_Vertices_of G1) \ {v} = {} by A4, XBOOLE_1:37;
hence G2 is removeVertex of G1,v by A1, A3, Def37; :: thesis: verum

end;

suppose v <> v1 ; :: thesis: G2 is removeVertex of G1,v

then not v in the_Vertices_of G1 by A4, TARSKI:def 1;
hence G2 is removeVertex of G1,v by A1, Lm11; :: thesis: verum

end;

end;

end;

suppose not v in the_Vertices_of G1 ; :: thesis: G2 is removeVertex of G1,v

hence G2 is removeVertex of G1,v by A1, Lm11; :: thesis: verum

end;

end;