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 G2 is removeEdge of G3,e by Th95;
hence G4 is removeEdge of G3,e by A1, Th101; :: thesis: verum