let G2 be _Graph; :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: ( not e in the_Edges_of G2 implies G2 is removeEdge of G1,e )
assume A1: not e in the_Edges_of G2 ; :: thesis: 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; :: thesis: verum