consider v being Vertex of G such that

the_Vertices_of G = {v} and

A4: the_Source_of G = (the_Edges_of G) --> v and

A5: the_Target_of G = (the_Edges_of G) --> v by GLIB_006:21;

the_Vertices_of G = {v} and

A4: the_Source_of G = (the_Edges_of G) --> v and

A5: the_Target_of G = (the_Edges_of G) --> v by GLIB_006:21;

now :: thesis: for e1, e2 being object st e1 in the_Edges_of G & e2 in the_Edges_of G holds

e1 = e2

hence
the_Edges_of G is trivial
by ZFMISC_1:def 10; :: thesis: verume1 = e2

let e1, e2 be object ; :: thesis: ( e1 in the_Edges_of G & e2 in the_Edges_of G implies e1 = e2 )

assume A6: ( e1 in the_Edges_of G & e2 in the_Edges_of G ) ; :: thesis: e1 = e2

then ( (the_Source_of G) . e1 = v & (the_Target_of G) . e1 = v & (the_Source_of G) . e2 = v & (the_Target_of G) . e2 = v ) by A4, A5, FUNCOP_1:7;

then ( e1 DJoins v,v,G & e2 DJoins v,v,G ) by A6, GLIB_000:def 14;

hence e1 = e2 by GLIB_000:def 21; :: thesis: verum

end;assume A6: ( e1 in the_Edges_of G & e2 in the_Edges_of G ) ; :: thesis: e1 = e2

then ( (the_Source_of G) . e1 = v & (the_Target_of G) . e1 = v & (the_Source_of G) . e2 = v & (the_Target_of G) . e2 = v ) by A4, A5, FUNCOP_1:7;

then ( e1 DJoins v,v,G & e2 DJoins v,v,G ) by A6, GLIB_000:def 14;

hence e1 = e2 by GLIB_000:def 21; :: thesis: verum