let G1 be _Graph; :: thesis: for e being set
for G2 being removeEdge 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 removeEdge of G1,e holds
( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = (the_Edges_of G1) \ {e} )
let G2 be removeEdge 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 E = (the_Edges_of G1) \ {e};
reconsider E = (the_Edges_of G1) \ {e} as Subset of (G1 .edgesBetween V) by Th34;
G2 is inducedSubgraph of G1,V,E ;
hence ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = (the_Edges_of G1) \ {e} ) by Def37; :: thesis: verum