let G1 be _Graph; :: thesis:
let G2 be Subgraph of G1; :: thesis:
let E2 be RepDEdgeSelection of G2; :: thesis:
set A = { { e where e is Element of the_Edges_of G1 : e DJoins v1,v2,G1 } where v1, v2 is Vertex of G1 : ( ex e0 being object st e0 DJoins v1,v2,G1 & ( for e0 being object st e0 DJoins v1,v2,G1 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 G1 : e DJoins v1,v2,G1 } where v1, v2 is Vertex of G1 : ( ex e0 being object st e0 DJoins v1,v2,G1 & ( for e0 being object st e0 DJoins v1,v2,G1 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 G1 : e DJoins v1,v2,G1 } where v1, v2 is Vertex of G1 : ( ex e0 being object st e0 DJoins v1,v2,G1 & ( for e0 being object st e0 DJoins v1,v2,G1 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 G1 : e DJoins v1,v2,G1 } where v1, v2 is Vertex of G1 : ( ex e0 being object st e0 DJoins v1,v2,G1 & ( for e0 being object st e0 DJoins v1,v2,G1 holds
not e0 in E2 ) ) } ; :: thesis:
then consider v1, v2 being Vertex of G1 such that
A3: x = { e where e is Element of the_Edges_of G1 : e DJoins v1,v2,G1 } and
A4: ex e0 being object st e0 DJoins v1,v2,G1 and
for e0 being object st e0 DJoins v1,v2,G1 holds
not e0 in E2 ;
reconsider B = x as set by A3;
consider e0 being object such that
A5: e0 DJoins v1,v2,G1 by A4;
reconsider e0 = e0 as Element of the_Edges_of G1 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 G1 : e DJoins v1,v2,G1 } where v1, v2 is Vertex of G1 : ( ex e0 being object st e0 DJoins v1,v2,G1 & ( for e0 being object st e0 DJoins v1,v2,G1 holds
not e0 in E2 ) ) } & ( for x being object st x in { { e where e is Element of the_Edges_of G1 : e DJoins v1,v2,G1 } where v1, v2 is Vertex of G1 : ( ex e0 being object st e0 DJoins v1,v2,G1 & ( for e0 being object st e0 DJoins v1,v2,G1 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 G1

proof

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 G1 such that
A9: C = { e where e is Element of the_Edges_of G1 : e DJoins v1,v2,G1 } and
ex e0 being object st e0 DJoins v1,v2,G1 and
for e0 being object st e0 DJoins v1,v2,G1 holds
not e0 in E2 by A6, A7;
e in C0 by A7, A8;
then consider e2 being Element of the_Edges_of G1 such that
A10: ( e = e2 & e2 DJoins v1,v2,G1 ) by A8, A9;
thus e in the_Edges_of G1 by A10, GLIB_000:def 14; :: thesis:

end;

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

proof

let v, w, e0 be object ; :: thesis:
A12: ( v is set & w is set ) by TARSKI:1;
assume A13: e0 DJoins v,w,G1 ; :: thesis:

per cases ;

suppose ex e1 being object st
( e1 DJoins v,w,G1 & e1 in E2 ) ; :: thesis:

then consider e1 being object such that
A14: ( e1 DJoins v,w,G1 & e1 in E2 ) ;
e1 DJoins v,w,G2 by A12, A14, GLIB_000:73;
then consider e being object such that
A15: ( e DJoins v,w,G2 & e in E2 ) and
A16: for e8 being object st e8 DJoins v,w,G2 & e8 in E2 holds
e8 = e by Def6;
take e ; :: thesis:
thus A17: e DJoins v,w,G1 by A12, A15, GLIB_000:72; :: thesis:
thus e in E1 by A15, XBOOLE_0:def 3; :: thesis:
let e9 be object ; :: thesis:
assume A18: ( e9 DJoins v,w,G1 & e9 in E1 ) ; :: thesis:
not e9 in rng f

proof

assume e9 in rng f ; :: thesis:
then consider C being object such that
A19: ( C in dom f & f . C = e9 ) by FUNCT_1:def 3;
consider v1, v2 being Vertex of G1 such that
A20: C = { k where k is Element of the_Edges_of G1 : k DJoins v1,v2,G1 } and
ex k0 being object st k0 DJoins v1,v2,G1 and
A21: for k0 being object st k0 DJoins v1,v2,G1 holds
not k0 in E2 by A6, A19;
consider C0 being non empty set such that
A22: ( C = C0 & f . C = the Element of C0 ) by A6, A19;
e9 in C0 by A19, A22;
then consider k being Element of the_Edges_of G1 such that
A23: ( e9 = k & k DJoins v1,v2,G1 ) by A20, A22;
( v1 = v & v2 = w ) by A18, A23, GLIB_000:125;
hence contradiction by A15, A17, A21; :: thesis:

end;

then A24: e9 in E2 by A18, XBOOLE_0:def 3;
then e9 DJoins v,w,G2 by A12, A18, GLIB_000:73;
hence e9 = e by A16, A24; :: thesis:

end;

suppose A25: for e1 being object st e1 DJoins v,w,G1 holds
not e1 in E2 ; :: thesis:

e0 Joins v,w,G1 by A13, GLIB_000:16;
then A26: ( v is Vertex of G1 & w is Vertex of G1 ) by GLIB_000:13;
set B = { e where e is Element of the_Edges_of G1 : e DJoins v,w,G1 } ;
A27: { e where e is Element of the_Edges_of G1 : e DJoins v,w,G1 } in { { e where e is Element of the_Edges_of G1 : e DJoins v1,v2,G1 } where v1, v2 is Vertex of G1 : ( ex e0 being object st e0 DJoins v1,v2,G1 & ( for e0 being object st e0 DJoins v1,v2,G1 holds
not e0 in E2 ) ) } by A13, A25, A26;
then consider B0 being non empty set such that
A28: ( { e where e is Element of the_Edges_of G1 : e DJoins v,w,G1 } = B0 & f . { e where e is Element of the_Edges_of G1 : e DJoins v,w,G1 } = the Element of B0 ) by A6;
f . { e where e is Element of the_Edges_of G1 : e DJoins v,w,G1 } in { e where e is Element of the_Edges_of G1 : e DJoins v,w,G1 } by A28;
then consider e being Element of the_Edges_of G1 such that
A29: ( f . { e where e is Element of the_Edges_of G1 : e DJoins v,w,G1 } = e & e DJoins v,w,G1 ) ;
take e ; :: thesis:
thus e DJoins v,w,G1 by A29; :: thesis:
e in rng f by A6, A27, A29, FUNCT_1:3;
hence e in E1 by XBOOLE_0:def 3; :: thesis:
let e9 be object ; :: thesis:
assume A30: ( e9 DJoins v,w,G1 & e9 in E1 ) ; :: thesis:
then not e9 in E2 by A25;
then e9 in rng f by A30, XBOOLE_0:def 3;
then consider C being object such that
A31: ( C in dom f & f . C = e9 ) by FUNCT_1:def 3;
consider v1, v2 being Vertex of G1 such that
A32: C = { k where k is Element of the_Edges_of G1 : k DJoins v1,v2,G1 } and
ex k0 being object st k0 DJoins v1,v2,G1 and
for k0 being object st k0 DJoins v1,v2,G1 holds
not k0 in E2 by A6, A31;
consider C0 being non empty set such that
A33: ( C = C0 & f . C = the Element of C0 ) by A6, A31;
f . C in C0 by A33;
then consider k being Element of the_Edges_of G1 such that
A34: ( f . C = k & k DJoins v1,v2,G1 ) by A32, A33;
for x being object holds
( x in { e where e is Element of the_Edges_of G1 : e DJoins v,w,G1 } iff x in C0 )

proof

let x be object ; :: thesis:
A35: ( v1 = v & v2 = w ) by A30, A31, A34, GLIB_000:125;
thus ( x in { e where e is Element of the_Edges_of G1 : e DJoins v,w,G1 } implies x in C0 ) by A32, A33, A35; :: thesis:
assume x in C0 ; :: thesis:
then consider k being Element of the_Edges_of G1 such that
A36: ( x = k & k DJoins v1,v2,G1 ) by A32, A33;
thus x in { e where e is Element of the_Edges_of G1 : e DJoins v,w,G1 } by A35, A36; :: thesis:

end;

hence e9 = e by A29, A31, A33, TARSKI:2; :: thesis:

end;

then reconsider E1 = E1 as RepDEdgeSelection of G1 by Def6;
take E1 ; :: thesis:
for x being object holds
( x in E2 iff ( x in E1 & x in the_Edges_of G2 ) )

proof

let x be object ; :: thesis:
thus ( x in E2 implies ( x in E1 & x in the_Edges_of G2 ) ) by TARSKI:def 3, XBOOLE_1:7; :: thesis:
assume A37: ( x in E1 & x in the_Edges_of G2 ) ; :: thesis:
not x in rng f

proof

assume x in rng f ; :: thesis:
then consider C being object such that
A38: ( C in dom f & f . C = x ) by FUNCT_1:def 3;
consider v1, v2 being Vertex of G1 such that
A39: C = { e where e is Element of the_Edges_of G1 : e DJoins v1,v2,G1 } and
ex e0 being object st e0 DJoins v1,v2,G1 and
A40: for e0 being object st e0 DJoins v1,v2,G1 holds
not e0 in E2 by A6, A38;
consider C0 being non empty set such that
A41: ( C = C0 & f . C = the Element of C0 ) by A6, A38;
f . C in C0 by A41;
then consider e being Element of the_Edges_of G1 such that
A42: ( f . C = e & e DJoins v1,v2,G1 ) by A39, A41;
x DJoins v1,v2,G2 by A37, A38, A42, GLIB_000:73;
then consider e1 being object such that
A43: ( e1 DJoins v1,v2,G2 & e1 in E2 ) and
for e9 being object st e9 DJoins v1,v2,G2 & e9 in E2 holds
e9 = e1 by Def6;
thus contradiction by A40, A43, GLIB_000:72; :: thesis:

end;

hence x in E2 by A37, XBOOLE_0:def 3; :: thesis:

end;

hence E2 = E1 /\ (the_Edges_of G2) by XBOOLE_0:def 4; :: thesis: