let G2, G3 be _Graph; :: thesis: for v1, e, v2 being object
for G1 being addEdge of G2,v1,e,v2 st G2 == G3 holds
G1 is addEdge of G3,v1,e,v2
let v1, e, v2 be object ; :: thesis: for G1 being addEdge of G2,v1,e,v2 st G2 == G3 holds
G1 is addEdge of G3,v1,e,v2
let G1 be addEdge of G2,v1,e,v2; :: thesis: ( G2 == G3 implies G1 is addEdge of G3,v1,e,v2 )
assume A1: G2 == G3 ; :: thesis: G1 is addEdge of G3,v1,e,v2
then A2: ( the_Vertices_of G3 = the_Vertices_of G2 & the_Edges_of G3 = the_Edges_of G2 & the_Target_of G3 = the_Target_of G2 & the_Source_of G3 = the_Source_of G2 ) by GLIB_000:def 34;

per cases ( ( v1 in the_Vertices_of G2 & v2 in the_Vertices_of G2 & not e in the_Edges_of G2 ) or not v1 in the_Vertices_of G2 or not v2 in the_Vertices_of G2 or e in the_Edges_of G2 ) ;

suppose A3: ( v1 in the_Vertices_of G2 & v2 in the_Vertices_of G2 & not e in the_Edges_of G2 ) ; :: thesis: G1 is addEdge of G3,v1,e,v2

then A4: ( the_Vertices_of G1 = the_Vertices_of G3 & the_Edges_of G1 = (the_Edges_of G3) \/ {e} & the_Source_of G1 = (the_Source_of G3) +* (e .--> v1) & the_Target_of G1 = (the_Target_of G3) +* (e .--> v2) ) by A2, GLIB_006:def 11;
G2 is Supergraph of G3 by A1, GLIB_006:58;
then G1 is Supergraph of G3 by GLIB_006:62;
hence G1 is addEdge of G3,v1,e,v2 by A2, A3, A4, GLIB_006:def 11; :: thesis: verum

end;

suppose A5: ( not v1 in the_Vertices_of G2 or not v2 in the_Vertices_of G2 or e in the_Edges_of G2 ) ; :: thesis: G1 is addEdge of G3,v1,e,v2

then G1 == G2 by GLIB_006:def 11;
then A6: G1 == G3 by A1, GLIB_000:85;
then G1 is Supergraph of G3 by GLIB_006:58;
hence G1 is addEdge of G3,v1,e,v2 by A2, A5, A6, GLIB_006:def 11; :: thesis: verum

end;

end;