let G1 be _Graph; :: thesis: for G2 being Subgraph of G1

for E2 being RepEdgeSelection of G2 ex E1 being RepEdgeSelection of G1 st E2 = E1 /\ (the_Edges_of G2)

let G2 be Subgraph of G1; :: thesis: for E2 being RepEdgeSelection of G2 ex E1 being RepEdgeSelection of G1 st E2 = E1 /\ (the_Edges_of G2)

let E2 be RepEdgeSelection of G2; :: thesis: ex E1 being RepEdgeSelection of G1 st E2 = E1 /\ (the_Edges_of G2)

set A = { { e where e is Element of the_Edges_of G1 : e Joins v1,v2,G1 } where v1, v2 is Vertex of G1 : ( ex e0 being object st e0 Joins v1,v2,G1 & ( for e0 being object st e0 Joins v1,v2,G1 holds

not e0 in E2 ) ) } ;

defpred S_{1}[ 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 Joins v1,v2,G1 } where v1, v2 is Vertex of G1 : ( ex e0 being object st e0 Joins v1,v2,G1 & ( for e0 being object st e0 Joins v1,v2,G1 holds

not e0 in E2 ) ) } & S_{1}[x,y1] & S_{1}[x,y2] holds

y1 = y2 ;

A2: for x being object st x in { { e where e is Element of the_Edges_of G1 : e Joins v1,v2,G1 } where v1, v2 is Vertex of G1 : ( ex e0 being object st e0 Joins v1,v2,G1 & ( for e0 being object st e0 Joins v1,v2,G1 holds

not e0 in E2 ) ) } holds

ex y being object st S_{1}[x,y]

A6: ( dom f = { { e where e is Element of the_Edges_of G1 : e Joins v1,v2,G1 } where v1, v2 is Vertex of G1 : ( ex e0 being object st e0 Joins v1,v2,G1 & ( for e0 being object st e0 Joins 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 Joins v1,v2,G1 } where v1, v2 is Vertex of G1 : ( ex e0 being object st e0 Joins v1,v2,G1 & ( for e0 being object st e0 Joins v1,v2,G1 holds

not e0 in E2 ) ) } holds

S_{1}[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

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 Joins v,w,G1 holds

ex e being object st

( e Joins v,w,G1 & e in E1 & ( for e9 being object st e9 Joins v,w,G1 & e9 in E1 holds

e9 = e ) )

take E1 ; :: thesis: E2 = E1 /\ (the_Edges_of G2)

for x being object holds

( x in E2 iff ( x in E1 & x in the_Edges_of G2 ) )

for E2 being RepEdgeSelection of G2 ex E1 being RepEdgeSelection of G1 st E2 = E1 /\ (the_Edges_of G2)

let G2 be Subgraph of G1; :: thesis: for E2 being RepEdgeSelection of G2 ex E1 being RepEdgeSelection of G1 st E2 = E1 /\ (the_Edges_of G2)

let E2 be RepEdgeSelection of G2; :: thesis: ex E1 being RepEdgeSelection of G1 st E2 = E1 /\ (the_Edges_of G2)

set A = { { e where e is Element of the_Edges_of G1 : e Joins v1,v2,G1 } where v1, v2 is Vertex of G1 : ( ex e0 being object st e0 Joins v1,v2,G1 & ( for e0 being object st e0 Joins v1,v2,G1 holds

not e0 in E2 ) ) } ;

defpred S

( $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 Joins v1,v2,G1 } where v1, v2 is Vertex of G1 : ( ex e0 being object st e0 Joins v1,v2,G1 & ( for e0 being object st e0 Joins v1,v2,G1 holds

not e0 in E2 ) ) } & S

y1 = y2 ;

A2: for x being object st x in { { e where e is Element of the_Edges_of G1 : e Joins v1,v2,G1 } where v1, v2 is Vertex of G1 : ( ex e0 being object st e0 Joins v1,v2,G1 & ( for e0 being object st e0 Joins v1,v2,G1 holds

not e0 in E2 ) ) } holds

ex y being object st S

proof

consider f being Function such that
let x be object ; :: thesis: ( x in { { e where e is Element of the_Edges_of G1 : e Joins v1,v2,G1 } where v1, v2 is Vertex of G1 : ( ex e0 being object st e0 Joins v1,v2,G1 & ( for e0 being object st e0 Joins v1,v2,G1 holds

not e0 in E2 ) ) } implies ex y being object st S_{1}[x,y] )

assume x in { { e where e is Element of the_Edges_of G1 : e Joins v1,v2,G1 } where v1, v2 is Vertex of G1 : ( ex e0 being object st e0 Joins v1,v2,G1 & ( for e0 being object st e0 Joins v1,v2,G1 holds

not e0 in E2 ) ) } ; :: thesis: ex y being object st S_{1}[x,y]

then consider v1, v2 being Vertex of G1 such that

A3: x = { e where e is Element of the_Edges_of G1 : e Joins v1,v2,G1 } and

A4: ex e0 being object st e0 Joins v1,v2,G1 and

for e0 being object st e0 Joins v1,v2,G1 holds

not e0 in E2 ;

reconsider B = x as set by A3;

consider e0 being object such that

A5: e0 Joins v1,v2,G1 by A4;

reconsider e0 = e0 as Element of the_Edges_of G1 by A5, GLIB_000:def 13;

e0 in B by A3, A5;

then reconsider B = B as non empty set ;

take the Element of B ; :: thesis: S_{1}[x, the Element of B]

take B ; :: thesis: ( x = B & the Element of B = the Element of B )

thus ( x = B & the Element of B = the Element of B ) ; :: thesis: verum

end;not e0 in E2 ) ) } implies ex y being object st S

assume x in { { e where e is Element of the_Edges_of G1 : e Joins v1,v2,G1 } where v1, v2 is Vertex of G1 : ( ex e0 being object st e0 Joins v1,v2,G1 & ( for e0 being object st e0 Joins v1,v2,G1 holds

not e0 in E2 ) ) } ; :: thesis: ex y being object st S

then consider v1, v2 being Vertex of G1 such that

A3: x = { e where e is Element of the_Edges_of G1 : e Joins v1,v2,G1 } and

A4: ex e0 being object st e0 Joins v1,v2,G1 and

for e0 being object st e0 Joins v1,v2,G1 holds

not e0 in E2 ;

reconsider B = x as set by A3;

consider e0 being object such that

A5: e0 Joins v1,v2,G1 by A4;

reconsider e0 = e0 as Element of the_Edges_of G1 by A5, GLIB_000:def 13;

e0 in B by A3, A5;

then reconsider B = B as non empty set ;

take the Element of B ; :: thesis: S

take B ; :: thesis: ( x = B & the Element of B = the Element of B )

thus ( x = B & the Element of B = the Element of B ) ; :: thesis: verum

A6: ( dom f = { { e where e is Element of the_Edges_of G1 : e Joins v1,v2,G1 } where v1, v2 is Vertex of G1 : ( ex e0 being object st e0 Joins v1,v2,G1 & ( for e0 being object st e0 Joins 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 Joins v1,v2,G1 } where v1, v2 is Vertex of G1 : ( ex e0 being object st e0 Joins v1,v2,G1 & ( for e0 being object st e0 Joins v1,v2,G1 holds

not e0 in E2 ) ) } holds

S

for e being object st e in rng f holds

e in the_Edges_of G1

proof

then A11:
rng f c= the_Edges_of G1
by TARSKI:def 3;
let e be object ; :: thesis: ( e in rng f implies e in the_Edges_of G1 )

assume e in rng f ; :: thesis: e in the_Edges_of G1

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 Joins v1,v2,G1 } and

ex e0 being object st e0 Joins v1,v2,G1 and

for e0 being object st e0 Joins 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 Joins v1,v2,G1 ) by A8, A9;

thus e in the_Edges_of G1 by A10, GLIB_000:def 13; :: thesis: verum

end;assume e in rng f ; :: thesis: e in the_Edges_of G1

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 Joins v1,v2,G1 } and

ex e0 being object st e0 Joins v1,v2,G1 and

for e0 being object st e0 Joins 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 Joins v1,v2,G1 ) by A8, A9;

thus e in the_Edges_of G1 by A10, GLIB_000:def 13; :: thesis: verum

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 Joins v,w,G1 holds

ex e being object st

( e Joins v,w,G1 & e in E1 & ( for e9 being object st e9 Joins v,w,G1 & e9 in E1 holds

e9 = e ) )

proof

then reconsider E1 = E1 as RepEdgeSelection of G1 by Def5;
let v, w, e0 be object ; :: thesis: ( e0 Joins v,w,G1 implies ex e being object st

( e Joins v,w,G1 & e in E1 & ( for e9 being object st e9 Joins v,w,G1 & e9 in E1 holds

e9 = e ) ) )

A12: ( v is set & w is set ) by TARSKI:1;

assume A13: e0 Joins v,w,G1 ; :: thesis: ex e being object st

( e Joins v,w,G1 & e in E1 & ( for e9 being object st e9 Joins v,w,G1 & e9 in E1 holds

e9 = e ) )

end;( e Joins v,w,G1 & e in E1 & ( for e9 being object st e9 Joins v,w,G1 & e9 in E1 holds

e9 = e ) ) )

A12: ( v is set & w is set ) by TARSKI:1;

assume A13: e0 Joins v,w,G1 ; :: thesis: ex e being object st

( e Joins v,w,G1 & e in E1 & ( for e9 being object st e9 Joins v,w,G1 & e9 in E1 holds

e9 = e ) )

per cases
( ex e1 being object st

( e1 Joins v,w,G1 & e1 in E2 ) or for e1 being object st e1 Joins v,w,G1 holds

not e1 in E2 ) ;

end;

( e1 Joins v,w,G1 & e1 in E2 ) or for e1 being object st e1 Joins v,w,G1 holds

not e1 in E2 ) ;

suppose
ex e1 being object st

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

( e Joins v,w,G1 & e in E1 & ( for e9 being object st e9 Joins v,w,G1 & e9 in E1 holds

e9 = e ) )

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

( e Joins v,w,G1 & e in E1 & ( for e9 being object st e9 Joins v,w,G1 & e9 in E1 holds

e9 = e ) )

then consider e1 being object such that

A14: ( e1 Joins v,w,G1 & e1 in E2 ) ;

e1 Joins v,w,G2 by A12, A14, GLIB_000:73;

then consider e being object such that

A15: ( e Joins v,w,G2 & e in E2 ) and

A16: for e8 being object st e8 Joins v,w,G2 & e8 in E2 holds

e8 = e by Def5;

take e ; :: thesis: ( e Joins v,w,G1 & e in E1 & ( for e9 being object st e9 Joins v,w,G1 & e9 in E1 holds

e9 = e ) )

thus A17: e Joins v,w,G1 by A12, A15, GLIB_000:72; :: thesis: ( e in E1 & ( for e9 being object st e9 Joins v,w,G1 & e9 in E1 holds

e9 = e ) )

thus e in E1 by A15, XBOOLE_0:def 3; :: thesis: for e9 being object st e9 Joins v,w,G1 & e9 in E1 holds

e9 = e

let e9 be object ; :: thesis: ( e9 Joins v,w,G1 & e9 in E1 implies e9 = e )

assume A18: ( e9 Joins v,w,G1 & e9 in E1 ) ; :: thesis: e9 = e

not e9 in rng f

then e9 Joins v,w,G2 by A12, A18, GLIB_000:73;

hence e9 = e by A16, A24; :: thesis: verum

end;A14: ( e1 Joins v,w,G1 & e1 in E2 ) ;

e1 Joins v,w,G2 by A12, A14, GLIB_000:73;

then consider e being object such that

A15: ( e Joins v,w,G2 & e in E2 ) and

A16: for e8 being object st e8 Joins v,w,G2 & e8 in E2 holds

e8 = e by Def5;

take e ; :: thesis: ( e Joins v,w,G1 & e in E1 & ( for e9 being object st e9 Joins v,w,G1 & e9 in E1 holds

e9 = e ) )

thus A17: e Joins v,w,G1 by A12, A15, GLIB_000:72; :: thesis: ( e in E1 & ( for e9 being object st e9 Joins v,w,G1 & e9 in E1 holds

e9 = e ) )

thus e in E1 by A15, XBOOLE_0:def 3; :: thesis: for e9 being object st e9 Joins v,w,G1 & e9 in E1 holds

e9 = e

let e9 be object ; :: thesis: ( e9 Joins v,w,G1 & e9 in E1 implies e9 = e )

assume A18: ( e9 Joins v,w,G1 & e9 in E1 ) ; :: thesis: e9 = e

not e9 in rng f

proof

then A24:
e9 in E2
by A18, XBOOLE_0:def 3;
assume
e9 in rng f
; :: thesis: contradiction

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 Joins v1,v2,G1 } and

ex k0 being object st k0 Joins v1,v2,G1 and

A21: for k0 being object st k0 Joins 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 Joins v1,v2,G1 ) by A20, A22;

( ( v1 = v & v2 = w ) or ( v1 = w & v2 = v ) ) by A18, A23, GLIB_000:15;

hence contradiction by A15, A17, A21, GLIB_000:14; :: thesis: verum

end;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 Joins v1,v2,G1 } and

ex k0 being object st k0 Joins v1,v2,G1 and

A21: for k0 being object st k0 Joins 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 Joins v1,v2,G1 ) by A20, A22;

( ( v1 = v & v2 = w ) or ( v1 = w & v2 = v ) ) by A18, A23, GLIB_000:15;

hence contradiction by A15, A17, A21, GLIB_000:14; :: thesis: verum

then e9 Joins v,w,G2 by A12, A18, GLIB_000:73;

hence e9 = e by A16, A24; :: thesis: verum

suppose A25:
for e1 being object st e1 Joins v,w,G1 holds

not e1 in E2 ; :: thesis: ex e being object st

( e Joins v,w,G1 & e in E1 & ( for e9 being object st e9 Joins v,w,G1 & e9 in E1 holds

e9 = e ) )

not e1 in E2 ; :: thesis: ex e being object st

( e Joins v,w,G1 & e in E1 & ( for e9 being object st e9 Joins v,w,G1 & e9 in E1 holds

e9 = e ) )

A26:
( v is Vertex of G1 & w is Vertex of G1 )
by A13, GLIB_000:13;

set B = { e where e is Element of the_Edges_of G1 : e Joins v,w,G1 } ;

A27: { e where e is Element of the_Edges_of G1 : e Joins v,w,G1 } in { { e where e is Element of the_Edges_of G1 : e Joins v1,v2,G1 } where v1, v2 is Vertex of G1 : ( ex e0 being object st e0 Joins v1,v2,G1 & ( for e0 being object st e0 Joins 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 Joins v,w,G1 } = B0 & f . { e where e is Element of the_Edges_of G1 : e Joins v,w,G1 } = the Element of B0 ) by A6;

f . { e where e is Element of the_Edges_of G1 : e Joins v,w,G1 } in { e where e is Element of the_Edges_of G1 : e Joins 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 Joins v,w,G1 } = e & e Joins v,w,G1 ) ;

take e ; :: thesis: ( e Joins v,w,G1 & e in E1 & ( for e9 being object st e9 Joins v,w,G1 & e9 in E1 holds

e9 = e ) )

thus e Joins v,w,G1 by A29; :: thesis: ( e in E1 & ( for e9 being object st e9 Joins v,w,G1 & e9 in E1 holds

e9 = e ) )

e in rng f by A6, A27, A29, FUNCT_1:3;

hence e in E1 by XBOOLE_0:def 3; :: thesis: for e9 being object st e9 Joins v,w,G1 & e9 in E1 holds

e9 = e

let e9 be object ; :: thesis: ( e9 Joins v,w,G1 & e9 in E1 implies e9 = e )

assume A30: ( e9 Joins v,w,G1 & e9 in E1 ) ; :: thesis: e9 = e

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 Joins v1,v2,G1 } and

ex k0 being object st k0 Joins v1,v2,G1 and

for k0 being object st k0 Joins 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 Joins v1,v2,G1 ) by A32, A33;

for x being object holds

( x in { e where e is Element of the_Edges_of G1 : e Joins v,w,G1 } iff x in C0 )

end;set B = { e where e is Element of the_Edges_of G1 : e Joins v,w,G1 } ;

A27: { e where e is Element of the_Edges_of G1 : e Joins v,w,G1 } in { { e where e is Element of the_Edges_of G1 : e Joins v1,v2,G1 } where v1, v2 is Vertex of G1 : ( ex e0 being object st e0 Joins v1,v2,G1 & ( for e0 being object st e0 Joins 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 Joins v,w,G1 } = B0 & f . { e where e is Element of the_Edges_of G1 : e Joins v,w,G1 } = the Element of B0 ) by A6;

f . { e where e is Element of the_Edges_of G1 : e Joins v,w,G1 } in { e where e is Element of the_Edges_of G1 : e Joins 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 Joins v,w,G1 } = e & e Joins v,w,G1 ) ;

take e ; :: thesis: ( e Joins v,w,G1 & e in E1 & ( for e9 being object st e9 Joins v,w,G1 & e9 in E1 holds

e9 = e ) )

thus e Joins v,w,G1 by A29; :: thesis: ( e in E1 & ( for e9 being object st e9 Joins v,w,G1 & e9 in E1 holds

e9 = e ) )

e in rng f by A6, A27, A29, FUNCT_1:3;

hence e in E1 by XBOOLE_0:def 3; :: thesis: for e9 being object st e9 Joins v,w,G1 & e9 in E1 holds

e9 = e

let e9 be object ; :: thesis: ( e9 Joins v,w,G1 & e9 in E1 implies e9 = e )

assume A30: ( e9 Joins v,w,G1 & e9 in E1 ) ; :: thesis: e9 = e

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 Joins v1,v2,G1 } and

ex k0 being object st k0 Joins v1,v2,G1 and

for k0 being object st k0 Joins 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 Joins v1,v2,G1 ) by A32, A33;

for x being object holds

( x in { e where e is Element of the_Edges_of G1 : e Joins v,w,G1 } iff x in C0 )

proof

hence
e9 = e
by A29, A31, A33, TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in { e where e is Element of the_Edges_of G1 : e Joins v,w,G1 } iff x in C0 )

A35: ( ( v1 = v & v2 = w ) or ( v1 = w & v2 = v ) ) by A30, A31, A34, GLIB_000:15;

then consider k being Element of the_Edges_of G1 such that

A37: ( x = k & k Joins v1,v2,G1 ) by A32, A33;

k Joins v,w,G1 by A35, A37, GLIB_000:14;

hence x in { e where e is Element of the_Edges_of G1 : e Joins v,w,G1 } by A37; :: thesis: verum

end;A35: ( ( v1 = v & v2 = w ) or ( v1 = w & v2 = v ) ) by A30, A31, A34, GLIB_000:15;

hereby :: thesis: ( x in C0 implies x in { e where e is Element of the_Edges_of G1 : e Joins v,w,G1 } )

assume
x in C0
; :: thesis: x in { e where e is Element of the_Edges_of G1 : e Joins v,w,G1 } assume
x in { e where e is Element of the_Edges_of G1 : e Joins v,w,G1 }
; :: thesis: x in C0

then consider k being Element of the_Edges_of G1 such that

A36: ( x = k & k Joins v,w,G1 ) ;

k Joins v1,v2,G1 by A35, A36, GLIB_000:14;

hence x in C0 by A32, A33, A36; :: thesis: verum

end;then consider k being Element of the_Edges_of G1 such that

A36: ( x = k & k Joins v,w,G1 ) ;

k Joins v1,v2,G1 by A35, A36, GLIB_000:14;

hence x in C0 by A32, A33, A36; :: thesis: verum

then consider k being Element of the_Edges_of G1 such that

A37: ( x = k & k Joins v1,v2,G1 ) by A32, A33;

k Joins v,w,G1 by A35, A37, GLIB_000:14;

hence x in { e where e is Element of the_Edges_of G1 : e Joins v,w,G1 } by A37; :: thesis: verum

take E1 ; :: thesis: E2 = E1 /\ (the_Edges_of G2)

for x being object holds

( x in E2 iff ( x in E1 & x in the_Edges_of G2 ) )

proof

hence
E2 = E1 /\ (the_Edges_of G2)
by XBOOLE_0:def 4; :: thesis: verum
let x be object ; :: thesis: ( x in E2 iff ( x in E1 & x in the_Edges_of G2 ) )

thus ( x in E2 implies ( x in E1 & x in the_Edges_of G2 ) ) by TARSKI:def 3, XBOOLE_1:7; :: thesis: ( x in E1 & x in the_Edges_of G2 implies x in E2 )

assume A38: ( x in E1 & x in the_Edges_of G2 ) ; :: thesis: x in E2

not x in rng f

end;thus ( x in E2 implies ( x in E1 & x in the_Edges_of G2 ) ) by TARSKI:def 3, XBOOLE_1:7; :: thesis: ( x in E1 & x in the_Edges_of G2 implies x in E2 )

assume A38: ( x in E1 & x in the_Edges_of G2 ) ; :: thesis: x in E2

not x in rng f

proof

hence
x in E2
by A38, XBOOLE_0:def 3; :: thesis: verum
assume
x in rng f
; :: thesis: contradiction

then consider C being object such that

A39: ( C in dom f & f . C = x ) by FUNCT_1:def 3;

consider v1, v2 being Vertex of G1 such that

A40: C = { e where e is Element of the_Edges_of G1 : e Joins v1,v2,G1 } and

ex e0 being object st e0 Joins v1,v2,G1 and

A41: for e0 being object st e0 Joins v1,v2,G1 holds

not e0 in E2 by A6, A39;

consider C0 being non empty set such that

A42: ( C = C0 & f . C = the Element of C0 ) by A6, A39;

f . C in C0 by A42;

then consider e being Element of the_Edges_of G1 such that

A43: ( f . C = e & e Joins v1,v2,G1 ) by A40, A42;

x Joins v1,v2,G2 by A38, A39, A43, GLIB_000:73;

then consider e1 being object such that

A44: ( e1 Joins v1,v2,G2 & e1 in E2 ) and

for e9 being object st e9 Joins v1,v2,G2 & e9 in E2 holds

e9 = e1 by Def5;

thus contradiction by A41, A44, GLIB_000:72; :: thesis: verum

end;then consider C being object such that

A39: ( C in dom f & f . C = x ) by FUNCT_1:def 3;

consider v1, v2 being Vertex of G1 such that

A40: C = { e where e is Element of the_Edges_of G1 : e Joins v1,v2,G1 } and

ex e0 being object st e0 Joins v1,v2,G1 and

A41: for e0 being object st e0 Joins v1,v2,G1 holds

not e0 in E2 by A6, A39;

consider C0 being non empty set such that

A42: ( C = C0 & f . C = the Element of C0 ) by A6, A39;

f . C in C0 by A42;

then consider e being Element of the_Edges_of G1 such that

A43: ( f . C = e & e Joins v1,v2,G1 ) by A40, A42;

x Joins v1,v2,G2 by A38, A39, A43, GLIB_000:73;

then consider e1 being object such that

A44: ( e1 Joins v1,v2,G2 & e1 in E2 ) and

for e9 being object st e9 Joins v1,v2,G2 & e9 in E2 holds

e9 = e1 by Def5;

thus contradiction by A41, A44, GLIB_000:72; :: thesis: verum