let G be non-multi _Graph; :: thesis: for E being RepEdgeSelection of G holds E = the_Edges_of G

let E be RepEdgeSelection of G; :: thesis: E = the_Edges_of G

for e being object st e in the_Edges_of G holds

e in E

hence E = the_Edges_of G by XBOOLE_0:def 10; :: thesis: verum

let E be RepEdgeSelection of G; :: thesis: E = the_Edges_of G

for e being object st e in the_Edges_of G holds

e in E

proof

then
the_Edges_of G c= E
by TARSKI:def 3;
let e be object ; :: thesis: ( e in the_Edges_of G implies e in E )

set v = (the_Source_of G) . e;

set w = (the_Target_of G) . e;

assume e in the_Edges_of G ; :: thesis: e in E

then A1: e Joins (the_Source_of G) . e,(the_Target_of G) . e,G by GLIB_000:def 13;

then consider e2 being object such that

A2: ( e2 Joins (the_Source_of G) . e,(the_Target_of G) . e,G & e2 in E ) and

for e9 being object st e9 Joins (the_Source_of G) . e,(the_Target_of G) . e,G & e9 in E holds

e9 = e2 by Def5;

thus e in E by A1, A2, GLIB_000:def 20; :: thesis: verum

end;set v = (the_Source_of G) . e;

set w = (the_Target_of G) . e;

assume e in the_Edges_of G ; :: thesis: e in E

then A1: e Joins (the_Source_of G) . e,(the_Target_of G) . e,G by GLIB_000:def 13;

then consider e2 being object such that

A2: ( e2 Joins (the_Source_of G) . e,(the_Target_of G) . e,G & e2 in E ) and

for e9 being object st e9 Joins (the_Source_of G) . e,(the_Target_of G) . e,G & e9 in E holds

e9 = e2 by Def5;

thus e in E by A1, A2, GLIB_000:def 20; :: thesis: verum

hence E = the_Edges_of G by XBOOLE_0:def 10; :: thesis: verum