let G1 be non _trivial _Graph; :: thesis: for v being Vertex of G1
for G2 being removeVertex of G1,v holds
( the_Vertices_of G2 = (the_Vertices_of G1) \ {v} & the_Edges_of G2 = G1 .edgesBetween ((the_Vertices_of G1) \ {v}) )
let v be Vertex of G1; :: thesis: for G2 being removeVertex of G1,v holds
( the_Vertices_of G2 = (the_Vertices_of G1) \ {v} & the_Edges_of G2 = G1 .edgesBetween ((the_Vertices_of G1) \ {v}) )
let G2 be removeVertex of G1,v; :: thesis: ( the_Vertices_of G2 = (the_Vertices_of G1) \ {v} & the_Edges_of G2 = G1 .edgesBetween ((the_Vertices_of G1) \ {v}) )
set VG = the_Vertices_of G1;
set V = (the_Vertices_of G1) \ {v};

now :: thesis: not (the_Vertices_of G1) \ {v} is empty

assume (the_Vertices_of G1) \ {v} is empty ; :: thesis: contradiction
then the_Vertices_of G1 c= {v} by XBOOLE_1:37;
then the_Vertices_of G1 = {v} by ZFMISC_1:33;
then card (the_Vertices_of G1) = 1 by CARD_1:30;
hence contradiction by Def19; :: thesis: verum

end;

then reconsider V = (the_Vertices_of G1) \ {v} as non empty Subset of (the_Vertices_of G1) ;
G2 is inducedSubgraph of G1,V ;
hence ( the_Vertices_of G2 = (the_Vertices_of G1) \ {v} & the_Edges_of G2 = G1 .edgesBetween ((the_Vertices_of G1) \ {v}) ) by Def37; :: thesis: verum