let G, G2 be _Graph; :: thesis: for v1, e, v2 being object
for G1 being addEdge of G,v1,e,v2 st G1 == G2 holds
G2 is addEdge of G,v1,e,v2
let v1, e, v2 be object ; :: thesis: for G1 being addEdge of G,v1,e,v2 st G1 == G2 holds
G2 is addEdge of G,v1,e,v2
let G1 be addEdge of G,v1,e,v2; :: thesis: ( G1 == G2 implies G2 is addEdge of G,v1,e,v2 )
assume A1: G1 == G2 ; :: thesis: G2 is addEdge of G,v1,e,v2

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

suppose A2: ( v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G ) ; :: thesis: G2 is addEdge of G,v1,e,v2

then ( the_Vertices_of G1 = the_Vertices_of G & the_Edges_of G1 = (the_Edges_of G) \/ {e} & the_Source_of G1 = (the_Source_of G) +* (e .--> v1) & the_Target_of G1 = (the_Target_of G) +* (e .--> v2) ) by Def11;
then A3: ( the_Vertices_of G2 = the_Vertices_of G & the_Edges_of G2 = (the_Edges_of G) \/ {e} & the_Source_of G2 = (the_Source_of G) +* (e .--> v1) & the_Target_of G2 = (the_Target_of G) +* (e .--> v2) ) by A1, GLIB_000:def 34;
G2 is Supergraph of G1 by A1, Th62;
then G2 is Supergraph of G by Th66;
hence G2 is addEdge of G,v1,e,v2 by A2, A3, Def11; :: thesis: verum

end;

suppose A4: ( not v1 in the_Vertices_of G or not v2 in the_Vertices_of G or e in the_Edges_of G ) ; :: thesis: G2 is addEdge of G,v1,e,v2

then G == G1 by Def11;
then A5: G == G2 by A1, GLIB_000:85;
then G2 is Supergraph of G by Th62;
hence G2 is addEdge of G,v1,e,v2 by A4, A5, Def11; :: thesis: verum

end;

end;