let G be _Graph; :: thesis: for E2 being RepEdgeSelection of G ex E1 being RepDEdgeSelection of G st E2 c= E1

let E2 be RepEdgeSelection of G; :: thesis: ex E1 being RepDEdgeSelection of G st E2 c= E1

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_{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 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_{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 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_{1}[x,y]

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_{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 G

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 ) )

take E1 ; :: thesis: E2 c= E1

thus E2 c= E1 by XBOOLE_1:7; :: thesis: verum

let E2 be RepEdgeSelection of G; :: thesis: ex E1 being RepDEdgeSelection of G st E2 c= E1

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

( $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

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

proof

consider f being Function such that
let x be object ; :: thesis: ( 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 ) ) } implies ex y being object st S_{1}[x,y] )

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: ex y being object st S_{1}[x,y]

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: 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 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: ex y being object st S

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: 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 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

for e being object st e in rng f holds

e in the_Edges_of G

proof

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

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

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: verum

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

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: verum

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 ) )

proof

then reconsider E1 = E1 as RepDEdgeSelection of G by Def6;
let v, w, e0 be object ; :: thesis: ( e0 DJoins v,w,G implies 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 ) ) )

assume A11: e0 DJoins v,w,G ; :: thesis: 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 ) )

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;

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

e9 = e ) ) )

assume A11: e0 DJoins v,w,G ; :: thesis: 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 ) )

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;

per cases
( e2 DJoins v,w,G or ( e2 DJoins w,v,G & not e2 DJoins v,w,G ) )
by A12, GLIB_000:16;

end;

suppose A14:
e2 DJoins v,w,G
; :: thesis: 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 ) )

( e DJoins v,w,G & e in E1 & ( for e9 being object st e9 DJoins v,w,G & e9 in E1 holds

e9 = e ) )

take
e2
; :: thesis: ( e2 DJoins v,w,G & e2 in E1 & ( for e9 being object st e9 DJoins v,w,G & e9 in E1 holds

e9 = e2 ) )

thus ( e2 DJoins v,w,G & e2 in E1 ) by A12, A14, TARSKI:def 3, XBOOLE_1:7; :: thesis: for e9 being object st e9 DJoins v,w,G & e9 in E1 holds

e9 = e2

let e9 be object ; :: thesis: ( e9 DJoins v,w,G & e9 in E1 implies e9 = e2 )

assume A15: ( e9 DJoins v,w,G & e9 in E1 ) ; :: thesis: e9 = e2

not e9 in rng f

e9 Joins v,w,G by A15, GLIB_000:16;

hence e9 = e2 by A13, A21; :: thesis: verum

end;e9 = e2 ) )

thus ( e2 DJoins v,w,G & e2 in E1 ) by A12, A14, TARSKI:def 3, XBOOLE_1:7; :: thesis: for e9 being object st e9 DJoins v,w,G & e9 in E1 holds

e9 = e2

let e9 be object ; :: thesis: ( e9 DJoins v,w,G & e9 in E1 implies e9 = e2 )

assume A15: ( e9 DJoins v,w,G & e9 in E1 ) ; :: thesis: e9 = e2

not e9 in rng f

proof

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

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: verum

end;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: verum

e9 Joins v,w,G by A15, GLIB_000:16;

hence e9 = e2 by A13, A21; :: thesis: verum

suppose A22:
( e2 DJoins w,v,G & not e2 DJoins v,w,G )
; :: thesis: 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 ) )

( e DJoins v,w,G & e in E1 & ( for e9 being object st e9 DJoins v,w,G & e9 in E1 holds

e9 = e ) )

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

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: ( e DJoins v,w,G & e in E1 & ( for e9 being object st e9 DJoins v,w,G & e9 in E1 holds

e9 = e ) )

thus e DJoins v,w,G by A27; :: thesis: ( e in E1 & ( for e9 being object st e9 DJoins v,w,G & e9 in E1 holds

e9 = e ) )

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

hence e in E1 by XBOOLE_1:7, TARSKI:def 3; :: thesis: for e9 being object st e9 DJoins v,w,G & e9 in E1 holds

e9 = e

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

assume A28: ( e9 DJoins v,w,G & e9 in E1 ) ; :: thesis: e9 = e

not e9 in E2

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: verum

end;A23: for e9 being object st e9 DJoins v,w,G holds

not e9 in E2

proof

( v in the_Vertices_of G & w in the_Vertices_of G )
by A12, GLIB_000:13;
given e9 being object such that A24:
( e9 DJoins v,w,G & e9 in E2 )
; :: thesis: contradiction

e9 Joins v,w,G by A24, GLIB_000:16;

hence contradiction by A13, A22, A24; :: thesis: verum

end;e9 Joins v,w,G by A24, GLIB_000:16;

hence contradiction by A13, A22, A24; :: thesis: verum

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: ( e DJoins v,w,G & e in E1 & ( for e9 being object st e9 DJoins v,w,G & e9 in E1 holds

e9 = e ) )

thus e DJoins v,w,G by A27; :: thesis: ( e in E1 & ( for e9 being object st e9 DJoins v,w,G & e9 in E1 holds

e9 = e ) )

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

hence e in E1 by XBOOLE_1:7, TARSKI:def 3; :: thesis: for e9 being object st e9 DJoins v,w,G & e9 in E1 holds

e9 = e

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

assume A28: ( e9 DJoins v,w,G & e9 in E1 ) ; :: thesis: e9 = e

not e9 in E2

proof

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

e9 Joins v,w,G by A28, GLIB_000:16;

hence contradiction by A13, A22, A28, A29; :: thesis: verum

end;e9 Joins v,w,G by A28, GLIB_000:16;

hence contradiction by A13, A22, A28, A29; :: thesis: verum

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: verum

take E1 ; :: thesis: E2 c= E1

thus E2 c= E1 by XBOOLE_1:7; :: thesis: verum