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