let G be _Graph; :: thesis:
let E2 be RepEdgeSelection of G; :: thesis:
set A = { { e where e is Element of the_Edges_of G : e DJoins v1,v2,G } where v1, v2 is Vertex of G : ( ex e0 being object st e0 DJoins v1,v2,G & ( for e0 being object st e0 DJoins v1,v2,G holds
not e0 in E2 ) ) } ;
defpred S₁[ object , object ] means ex S being non empty set st
( $1 = S & $2 = the Element of S );
A1: for x, y1, y2 being object st x in { { e where e is Element of the_Edges_of G : e DJoins v1,v2,G } where v1, v2 is Vertex of G : ( ex e0 being object st e0 DJoins v1,v2,G & ( for e0 being object st e0 DJoins v1,v2,G holds
not e0 in E2 ) ) } & S₁[x,y1] & S₁[x,y2] holds
y1 = y2 ;
A2: for x being object st x in { { e where e is Element of the_Edges_of G : e DJoins v1,v2,G } where v1, v2 is Vertex of G : ( ex e0 being object st e0 DJoins v1,v2,G & ( for e0 being object st e0 DJoins v1,v2,G holds
not e0 in E2 ) ) } holds
ex y being object st S₁[x,y]

let x be object ; :: thesis:
assume x in { { e where e is Element of the_Edges_of G : e DJoins v1,v2,G } where v1, v2 is Vertex of G : ( ex e0 being object st e0 DJoins v1,v2,G & ( for e0 being object st e0 DJoins v1,v2,G holds
not e0 in E2 ) ) } ; :: thesis:
then consider v1, v2 being Vertex of G such that
A3: x = { e where e is Element of the_Edges_of G : e DJoins v1,v2,G } and
A4: ex e0 being object st e0 DJoins v1,v2,G and
for e0 being object st e0 DJoins v1,v2,G holds
not e0 in E2 ;
reconsider B = x as set by A3;
consider e0 being object such that
A5: e0 DJoins v1,v2,G by A4;
reconsider e0 = e0 as Element of the_Edges_of G by A5, GLIB_000:def 14;
e0 in B by A3, A5;
then reconsider B = B as non empty set ;
take the Element of B ; :: thesis:
take B ; :: thesis:
thus ( x = B & the Element of B = the Element of B ) ; :: thesis:

end;

consider f being Function such that
A6: ( dom f = { { e where e is Element of the_Edges_of G : e DJoins v1,v2,G } where v1, v2 is Vertex of G : ( ex e0 being object st e0 DJoins v1,v2,G & ( for e0 being object st e0 DJoins v1,v2,G holds
not e0 in E2 ) ) } & ( for x being object st x in { { e where e is Element of the_Edges_of G : e DJoins v1,v2,G } where v1, v2 is Vertex of G : ( ex e0 being object st e0 DJoins v1,v2,G & ( for e0 being object st e0 DJoins v1,v2,G holds
not e0 in E2 ) ) } holds
S₁[x,f . x] ) ) from FUNCT_1:sch 2(A1, A2);
for e being object st e in rng f holds
e in the_Edges_of G

let e be object ; :: thesis:
assume e in rng f ; :: thesis:
then consider C being object such that
A7: ( C in dom f & f . C = e ) by FUNCT_1:def 3;
consider C0 being non empty set such that
A8: ( C = C0 & f . C = the Element of C0 ) by A6, A7;
consider v1, v2 being Vertex of G such that
A9: C = { e where e is Element of the_Edges_of G : e DJoins v1,v2,G } and
ex e0 being object st e0 DJoins v1,v2,G and
for e0 being object st e0 DJoins v1,v2,G holds
not e0 in E2 by A6, A7;
e in C0 by A7, A8;
then consider e2 being Element of the_Edges_of G such that
A10: ( e = e2 & e2 DJoins v1,v2,G ) by A8, A9;
thus e in the_Edges_of G by A10, GLIB_000:def 14; :: thesis:

end;

then rng f c= the_Edges_of G by TARSKI:def 3;
then reconsider E1 = E2 \/ (rng f) as Subset of (the_Edges_of G) by XBOOLE_1:8;
for v, w, e0 being object st e0 DJoins v,w,G holds
ex e being object st
( e DJoins v,w,G & e in E1 & ( for e9 being object st e9 DJoins v,w,G & e9 in E1 holds
e9 = e ) )

let v, w, e0 be object ; :: thesis:
assume A11: e0 DJoins v,w,G ; :: thesis:
then e0 Joins v,w,G by GLIB_000:16;
then consider e2 being object such that
A12: ( e2 Joins v,w,G & e2 in E2 ) and
A13: for e8 being object st e8 Joins v,w,G & e8 in E2 holds
e8 = e2 by Def5;

assume e9 in rng f ; :: thesis:
then consider C being object such that
A16: ( C in dom f & f . C = e9 ) by FUNCT_1:def 3;
consider C0 being non empty set such that
A17: ( C = C0 & f . C = the Element of C0 ) by A6, A16;
consider v1, v2 being Vertex of G such that
A18: C = { e where e is Element of the_Edges_of G : e DJoins v1,v2,G } and
ex e0 being object st e0 DJoins v1,v2,G and
A19: for e0 being object st e0 DJoins v1,v2,G holds
not e0 in E2 by A6, A16;
e9 in C0 by A16, A17;
then consider e being Element of the_Edges_of G such that
A20: ( e9 = e & e DJoins v1,v2,G ) by A17, A18;
( v = v1 & w = v2 ) by A15, A20, Th6;
hence contradiction by A12, A14, A19; :: thesis:

end;

end;

set B = { e where e is Element of the_Edges_of G : e DJoins v,w,G } ;
A23: for e9 being object st e9 DJoins v,w,G holds
not e9 in E2

end;

( v in the_Vertices_of G & w in the_Vertices_of G ) by A12, GLIB_000:13;
then A25: { e where e is Element of the_Edges_of G : e DJoins v,w,G } in { { e where e is Element of the_Edges_of G : e DJoins v1,v2,G } where v1, v2 is Vertex of G : ( ex e0 being object st e0 DJoins v1,v2,G & ( for e0 being object st e0 DJoins v1,v2,G holds
not e0 in E2 ) ) } by A11, A23;
then consider B0 being non empty set such that
A26: ( { e where e is Element of the_Edges_of G : e DJoins v,w,G } = B0 & f . { e where e is Element of the_Edges_of G : e DJoins v,w,G } = the Element of B0 ) by A6;
f . { e where e is Element of the_Edges_of G : e DJoins v,w,G } in B0 by A26;
then consider e being Element of the_Edges_of G such that
A27: ( f . { e where e is Element of the_Edges_of G : e DJoins v,w,G } = e & e DJoins v,w,G ) by A26;
take e ; :: thesis:
thus e DJoins v,w,G by A27; :: thesis:
e in rng f by A6, A25, A27, FUNCT_1:3;
hence e in E1 by XBOOLE_1:7, TARSKI:def 3; :: thesis:
let e9 be object ; :: thesis:
assume A28: ( e9 DJoins v,w,G & e9 in E1 ) ; :: thesis:
not e9 in E2

end;

then e9 in rng f by A28, XBOOLE_0:def 3;
then consider C being object such that
A30: ( C in dom f & f . C = e9 ) by FUNCT_1:def 3;
consider C0 being non empty set such that
A31: ( C = C0 & f . C = the Element of C0 ) by A6, A30;
consider v1, v2 being Vertex of G such that
A32: C = { e1 where e1 is Element of the_Edges_of G : e1 DJoins v1,v2,G } and
ex e7 being object st e7 DJoins v1,v2,G and
for e7 being object st e7 DJoins v1,v2,G holds
not e7 in E2 by A6, A30;
e9 in C0 by A30, A31;
then consider e1 being Element of the_Edges_of G such that
A33: ( e9 = e1 & e1 DJoins v1,v2,G ) by A31, A32;
( v = v1 & w = v2 ) by A28, A33, Th6;
hence e9 = e by A27, A30, A32; :: thesis:

end;

then reconsider E1 = E1 as RepDEdgeSelection of G by Def6;
take E1 ; :: thesis:
thus E2 c= E1 by XBOOLE_1:7; :: thesis: