let G2 be _Graph; :: thesis: for v being object
for G1 being addAdjVertexAll of G2,v, {} holds the_Edges_of G2 = the_Edges_of G1
let v be object ; :: thesis: for G1 being addAdjVertexAll of G2,v, {} holds the_Edges_of G2 = the_Edges_of G1
let G1 be addAdjVertexAll of G2,v, {} ; :: thesis: the_Edges_of G2 = the_Edges_of G1

per cases ( ( {} c= the_Vertices_of G2 & not v in the_Vertices_of G2 ) or not {} c= the_Vertices_of G2 or v in the_Vertices_of G2 ) ;

suppose ( {} c= the_Vertices_of G2 & not v in the_Vertices_of G2 ) ; :: thesis: the_Edges_of G2 = the_Edges_of G1

then consider E being set such that
A1: ( card {} = card E & E misses the_Edges_of G2 ) and
A2: the_Edges_of G1 = (the_Edges_of G2) \/ E and
for v1 being object st v1 in {} holds
ex e1 being object st
( e1 in E & e1 Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 ) ) by Def4;
E = {} by A1;
hence the_Edges_of G2 = the_Edges_of G1 by A2; :: thesis: verum

end;

suppose ( not {} c= the_Vertices_of G2 or v in the_Vertices_of G2 ) ; :: thesis: the_Edges_of G2 = the_Edges_of G1

then G2 == G1 by Def4;
hence the_Edges_of G2 = the_Edges_of G1 by GLIB_000:def 34; :: thesis: verum

end;

end;