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 G1 == G2 ; :: thesis: G3 == G4
then G4 is removeEdge of G1,e by Th95;
hence G3 == G4 by Th93; :: thesis: verum