let G1 be _Graph; :: thesis: for E being set
for G2 being removeEdges of G1,E holds
( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = (the_Edges_of G1) \ E )
let E be set ; :: thesis: for G2 being removeEdges of G1,E holds
( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = (the_Edges_of G1) \ E )
let G2 be removeEdges of G1,E; :: thesis: ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = (the_Edges_of G1) \ E )
set V = the_Vertices_of G1;
the_Vertices_of G1 c= the_Vertices_of G1 ;
then reconsider V = the_Vertices_of G1 as non empty Subset of (the_Vertices_of G1) ;
set E2 = (the_Edges_of G1) \ E;
reconsider E2 = (the_Edges_of G1) \ E as Subset of (G1 .edgesBetween V) by Th34;
G2 is inducedSubgraph of G1,V,E2 ;
hence ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = (the_Edges_of G1) \ E ) by Def37; :: thesis: verum