let G2 be _Graph; :: thesis: for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 holds
( G1 == G2 iff e in the_Edges_of G2 )
let v1, v2 be Vertex of G2; :: thesis: for e being object
for G1 being addEdge of G2,v1,e,v2 holds
( G1 == G2 iff e in the_Edges_of G2 )
let e be object ; :: thesis: for G1 being addEdge of G2,v1,e,v2 holds
( G1 == G2 iff e in the_Edges_of G2 )
let G1 be addEdge of G2,v1,e,v2; :: thesis: ( G1 == G2 iff e in the_Edges_of G2 )

hereby :: thesis: ( e in the_Edges_of G2 implies G1 == G2 )

assume G1 == G2 ; :: thesis: e in the_Edges_of G2
then A1: the_Edges_of G1 = the_Edges_of G2 by GLIB_000:def 34;

per cases ( e in the_Edges_of G2 or not e in the_Edges_of G2 ) ;

suppose e in the_Edges_of G2 ; :: thesis: e in the_Edges_of G2

hence e in the_Edges_of G2 ; :: thesis: verum

end;

suppose not e in the_Edges_of G2 ; :: thesis: e in the_Edges_of G2

then (the_Edges_of G2) \/ {e} c= the_Edges_of G2 by A1, Def11;
hence e in the_Edges_of G2 by ZFMISC_1:39; :: thesis: verum

end;

end;

end;

thus ( e in the_Edges_of G2 implies G1 == G2 ) by Def11; :: thesis: verum