let G1 be _Graph; :: thesis: for V being set
for G2 being removeVertices of G1,V st V c< the_Vertices_of G1 holds
( the_Vertices_of G2 = (the_Vertices_of G1) \ V & the_Edges_of G2 = G1 .edgesBetween ((the_Vertices_of G1) \ V) )
let V be set ; :: thesis: for G2 being removeVertices of G1,V st V c< the_Vertices_of G1 holds
( the_Vertices_of G2 = (the_Vertices_of G1) \ V & the_Edges_of G2 = G1 .edgesBetween ((the_Vertices_of G1) \ V) )
let G2 be removeVertices of G1,V; :: thesis: ( V c< the_Vertices_of G1 implies ( the_Vertices_of G2 = (the_Vertices_of G1) \ V & the_Edges_of G2 = G1 .edgesBetween ((the_Vertices_of G1) \ V) ) )
set VG2 = (the_Vertices_of G1) \ V;
assume A1: V c< the_Vertices_of G1 ; :: thesis: ( the_Vertices_of G2 = (the_Vertices_of G1) \ V & the_Edges_of G2 = G1 .edgesBetween ((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;
hence contradiction by A1, XBOOLE_0:def 8; :: thesis: verum

end;

then reconsider VG2 = (the_Vertices_of G1) \ V as non empty Subset of (the_Vertices_of G1) ;
G2 is inducedSubgraph of G1,VG2 ;
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