let G2 be _Graph; for v1, v2 being Vertex of G2
for e being set
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 holds
G2 is removeEdge of G1,e
let v1, v2 be Vertex of G2; for e being set
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 holds
G2 is removeEdge of G1,e
let e be set ; for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 holds
G2 is removeEdge of G1,e
let G1 be addEdge of G2,v1,e,v2; ( not e in the_Edges_of G2 implies G2 is removeEdge of G1,e )
assume A1:
not e in the_Edges_of G2
; G2 is removeEdge of G1,e
then A2:
( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ {e} & the_Source_of G1 = (the_Source_of G2) +* (e .--> v1) & the_Target_of G1 = (the_Target_of G2) +* (e .--> v2) )
by Def11;
then A3:
(the_Edges_of G1) \ {e} = the_Edges_of G2
by A1, ZFMISC_1:117;
( not the_Vertices_of G1 is empty & 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) ;
A4:
G2 is Subgraph of G1
by Th61;
(the_Edges_of G1) \ {e} c= the_Edges_of G1
;
then
(the_Edges_of G1) \ {e} c= G1 .edgesBetween V
by GLIB_000:34;
hence
G2 is removeEdge of G1,e
by A2, A3, A4, GLIB_000:def 37; verum