let G be _Graph; :: thesis: for v1, e, v2 being object
for G1, G2 being addEdge of G,v1,e,v2 holds G1 == G2
let v1, e, v2 be object ; :: thesis: for G1, G2 being addEdge of G,v1,e,v2 holds G1 == G2
let G1, G2 be addEdge of G,v1,e,v2; :: thesis: G1 == G2

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 ( v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G ) ; :: thesis: G1 == G2

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) & 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 Def11;
hence G1 == G2 by GLIB_000:def 34; :: thesis: verum

end;

suppose ( not v1 in the_Vertices_of G or not v2 in the_Vertices_of G or e in the_Edges_of G ) ; :: thesis: G1 == G2

then ( G == G1 & G == G2 ) by Def11;
hence G1 == G2 by GLIB_000:85; :: thesis: verum

end;

end;