let G1, G3, G4 be _Graph; :: thesis: for e being set
for G2 being removeEdge of G1,e st G1 == G3 & G2 == G4 holds
G4 is removeEdge of G3,e
let e be set ; :: thesis: for G2 being removeEdge of G1,e st G1 == G3 & G2 == G4 holds
G4 is removeEdge of G3,e
let G2 be removeEdge of G1,e; :: thesis: ( G1 == G3 & G2 == G4 implies G4 is removeEdge of G3,e )
assume A1: ( G1 == G3 & G2 == G4 ) ; :: thesis: G4 is removeEdge of G3,e
then ( the_Vertices_of G1 = the_Vertices_of G3 & the_Edges_of G1 = the_Edges_of G3 ) by GLIB_000:def 34;
then G2 is removeEdge of G3,e by A1, GLIB_000:95;
hence G4 is removeEdge of G3,e by A1, GLIB_006:16; :: thesis: verum