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

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

set A = { { e where e is Element of the_Edges_of G : ( e Joins v1,v2,G & e in E1 ) } where v1, v2 is Vertex of G : ex e0 being object st e0 Joins v1,v2,G } ;

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 Joins v1,v2,G & e in E1 ) } where v1, v2 is Vertex of G : ex e0 being object st e0 Joins v1,v2,G } & 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 Joins v1,v2,G & e in E1 ) } where v1, v2 is Vertex of G : ex e0 being object st e0 Joins v1,v2,G } holds

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

A8: ( dom f = { { e where e is Element of the_Edges_of G : ( e Joins v1,v2,G & e in E1 ) } where v1, v2 is Vertex of G : ex e0 being object st e0 Joins v1,v2,G } & ( for x being object st x in { { e where e is Element of the_Edges_of G : ( e Joins v1,v2,G & e in E1 ) } where v1, v2 is Vertex of G : ex e0 being object st e0 Joins v1,v2,G } 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 E1

then reconsider E2 = rng f as Subset of (the_Edges_of G) by XBOOLE_1:1;

for v, w, e0 being object st e0 Joins v,w,G holds

ex e being object st

( e Joins v,w,G & e in E2 & ( for e9 being object st e9 Joins v,w,G & e9 in E2 holds

e9 = e ) )

take E2 ; :: thesis: E2 c= E1

thus E2 c= E1 by A13; :: thesis: verum

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

set A = { { e where e is Element of the_Edges_of G : ( e Joins v1,v2,G & e in E1 ) } where v1, v2 is Vertex of G : ex e0 being object st e0 Joins v1,v2,G } ;

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 Joins v1,v2,G & e in E1 ) } where v1, v2 is Vertex of G : ex e0 being object st e0 Joins v1,v2,G } & S

y1 = y2 ;

A2: for x being object st x in { { e where e is Element of the_Edges_of G : ( e Joins v1,v2,G & e in E1 ) } where v1, v2 is Vertex of G : ex e0 being object st e0 Joins v1,v2,G } 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 Joins v1,v2,G & e in E1 ) } where v1, v2 is Vertex of G : ex e0 being object st e0 Joins v1,v2,G } implies ex y being object st S_{1}[x,y] )

assume x in { { e where e is Element of the_Edges_of G : ( e Joins v1,v2,G & e in E1 ) } where v1, v2 is Vertex of G : ex e0 being object st e0 Joins v1,v2,G } ; :: 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 Joins v1,v2,G & e in E1 ) } and

A4: ex e0 being object st e0 Joins v1,v2,G ;

reconsider B = x as set by A3;

consider e0 being object such that

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

end;assume x in { { e where e is Element of the_Edges_of G : ( e Joins v1,v2,G & e in E1 ) } where v1, v2 is Vertex of G : ex e0 being object st e0 Joins v1,v2,G } ; :: 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 Joins v1,v2,G & e in E1 ) } and

A4: ex e0 being object st e0 Joins v1,v2,G ;

reconsider B = x as set by A3;

consider e0 being object such that

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

per cases
( e0 DJoins v1,v2,G or e0 DJoins v2,v1,G )
by A5, GLIB_000:16;

end;

suppose
e0 DJoins v1,v2,G
; :: thesis: ex y being object st S_{1}[x,y]

then consider e being object such that

A6: ( e DJoins v1,v2,G & e in E1 ) and

for e9 being object st e9 DJoins v1,v2,G & e9 in E1 holds

e9 = e by Def6;

( e in the_Edges_of G & e Joins v1,v2,G ) by A6, GLIB_000:16;

then e in B by A3, A6;

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;A6: ( e DJoins v1,v2,G & e in E1 ) and

for e9 being object st e9 DJoins v1,v2,G & e9 in E1 holds

e9 = e by Def6;

( e in the_Edges_of G & e Joins v1,v2,G ) by A6, GLIB_000:16;

then e in B by A3, A6;

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

suppose
e0 DJoins v2,v1,G
; :: thesis: ex y being object st S_{1}[x,y]

then consider e being object such that

A7: ( e DJoins v2,v1,G & e in E1 ) and

for e9 being object st e9 DJoins v2,v1,G & e9 in E1 holds

e9 = e by Def6;

( e in the_Edges_of G & e Joins v1,v2,G ) by A7, GLIB_000:16;

then e in B by A3, A7;

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;A7: ( e DJoins v2,v1,G & e in E1 ) and

for e9 being object st e9 DJoins v2,v1,G & e9 in E1 holds

e9 = e by Def6;

( e in the_Edges_of G & e Joins v1,v2,G ) by A7, GLIB_000:16;

then e in B by A3, A7;

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

A8: ( dom f = { { e where e is Element of the_Edges_of G : ( e Joins v1,v2,G & e in E1 ) } where v1, v2 is Vertex of G : ex e0 being object st e0 Joins v1,v2,G } & ( for x being object st x in { { e where e is Element of the_Edges_of G : ( e Joins v1,v2,G & e in E1 ) } where v1, v2 is Vertex of G : ex e0 being object st e0 Joins v1,v2,G } holds

S

for e being object st e in rng f holds

e in E1

proof

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

assume e in rng f ; :: thesis: e in E1

then consider C being object such that

A9: ( C in dom f & f . C = e ) by FUNCT_1:def 3;

consider C0 being non empty set such that

A10: ( C = C0 & f . C = the Element of C0 ) by A8, A9;

consider v1, v2 being Vertex of G such that

A11: C = { e2 where e2 is Element of the_Edges_of G : ( e2 Joins v1,v2,G & e2 in E1 ) } and

ex e8 being object st e8 Joins v1,v2,G by A8, A9;

e in C0 by A9, A10;

then consider e2 being Element of the_Edges_of G such that

A12: ( e = e2 & e2 Joins v1,v2,G & e2 in E1 ) by A10, A11;

thus e in E1 by A12; :: thesis: verum

end;assume e in rng f ; :: thesis: e in E1

then consider C being object such that

A9: ( C in dom f & f . C = e ) by FUNCT_1:def 3;

consider C0 being non empty set such that

A10: ( C = C0 & f . C = the Element of C0 ) by A8, A9;

consider v1, v2 being Vertex of G such that

A11: C = { e2 where e2 is Element of the_Edges_of G : ( e2 Joins v1,v2,G & e2 in E1 ) } and

ex e8 being object st e8 Joins v1,v2,G by A8, A9;

e in C0 by A9, A10;

then consider e2 being Element of the_Edges_of G such that

A12: ( e = e2 & e2 Joins v1,v2,G & e2 in E1 ) by A10, A11;

thus e in E1 by A12; :: thesis: verum

then reconsider E2 = rng f as Subset of (the_Edges_of G) by XBOOLE_1:1;

for v, w, e0 being object st e0 Joins v,w,G holds

ex e being object st

( e Joins v,w,G & e in E2 & ( for e9 being object st e9 Joins v,w,G & e9 in E2 holds

e9 = e ) )

proof

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

( e Joins v,w,G & e in E2 & ( for e9 being object st e9 Joins v,w,G & e9 in E2 holds

e9 = e ) ) )

assume A14: e0 Joins v,w,G ; :: thesis: ex e being object st

( e Joins v,w,G & e in E2 & ( for e9 being object st e9 Joins v,w,G & e9 in E2 holds

e9 = e ) )

set B = { e where e is Element of the_Edges_of G : ( e Joins v,w,G & e in E1 ) } ;

( v in the_Vertices_of G & w in the_Vertices_of G ) by A14, GLIB_000:13;

then A15: { e where e is Element of the_Edges_of G : ( e Joins v,w,G & e in E1 ) } in { { e where e is Element of the_Edges_of G : ( e Joins v1,v2,G & e in E1 ) } where v1, v2 is Vertex of G : ex e0 being object st e0 Joins v1,v2,G } by A14;

then consider B0 being non empty set such that

A16: ( { e where e is Element of the_Edges_of G : ( e Joins v,w,G & e in E1 ) } = B0 & f . { e where e is Element of the_Edges_of G : ( e Joins v,w,G & e in E1 ) } = the Element of B0 ) by A8;

f . { e where e is Element of the_Edges_of G : ( e Joins v,w,G & e in E1 ) } in { e where e is Element of the_Edges_of G : ( e Joins v,w,G & e in E1 ) } by A16;

then consider e being Element of the_Edges_of G such that

A17: ( f . { e where e is Element of the_Edges_of G : ( e Joins v,w,G & e in E1 ) } = e & e Joins v,w,G & e in E1 ) ;

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

e9 = e ) )

thus e Joins v,w,G by A17; :: thesis: ( e in E2 & ( for e9 being object st e9 Joins v,w,G & e9 in E2 holds

e9 = e ) )

thus e in E2 by A8, A15, A17, FUNCT_1:3; :: thesis: for e9 being object st e9 Joins v,w,G & e9 in E2 holds

e9 = e

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

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

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 G such that

A20: C = { e2 where e2 is Element of the_Edges_of G : ( e2 Joins v1,v2,G & e2 in E1 ) } and

ex e8 being object st e8 Joins v1,v2,G by A8, A19;

consider C0 being non empty set such that

A21: ( C = C0 & f . C = the Element of C0 ) by A8, A19;

e9 in C0 by A19, A21;

then consider e2 being Element of the_Edges_of G such that

A22: ( e9 = e2 & e2 Joins v1,v2,G & e2 in E1 ) by A20, A21;

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

e9 = e ) ) )

assume A14: e0 Joins v,w,G ; :: thesis: ex e being object st

( e Joins v,w,G & e in E2 & ( for e9 being object st e9 Joins v,w,G & e9 in E2 holds

e9 = e ) )

set B = { e where e is Element of the_Edges_of G : ( e Joins v,w,G & e in E1 ) } ;

( v in the_Vertices_of G & w in the_Vertices_of G ) by A14, GLIB_000:13;

then A15: { e where e is Element of the_Edges_of G : ( e Joins v,w,G & e in E1 ) } in { { e where e is Element of the_Edges_of G : ( e Joins v1,v2,G & e in E1 ) } where v1, v2 is Vertex of G : ex e0 being object st e0 Joins v1,v2,G } by A14;

then consider B0 being non empty set such that

A16: ( { e where e is Element of the_Edges_of G : ( e Joins v,w,G & e in E1 ) } = B0 & f . { e where e is Element of the_Edges_of G : ( e Joins v,w,G & e in E1 ) } = the Element of B0 ) by A8;

f . { e where e is Element of the_Edges_of G : ( e Joins v,w,G & e in E1 ) } in { e where e is Element of the_Edges_of G : ( e Joins v,w,G & e in E1 ) } by A16;

then consider e being Element of the_Edges_of G such that

A17: ( f . { e where e is Element of the_Edges_of G : ( e Joins v,w,G & e in E1 ) } = e & e Joins v,w,G & e in E1 ) ;

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

e9 = e ) )

thus e Joins v,w,G by A17; :: thesis: ( e in E2 & ( for e9 being object st e9 Joins v,w,G & e9 in E2 holds

e9 = e ) )

thus e in E2 by A8, A15, A17, FUNCT_1:3; :: thesis: for e9 being object st e9 Joins v,w,G & e9 in E2 holds

e9 = e

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

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

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 G such that

A20: C = { e2 where e2 is Element of the_Edges_of G : ( e2 Joins v1,v2,G & e2 in E1 ) } and

ex e8 being object st e8 Joins v1,v2,G by A8, A19;

consider C0 being non empty set such that

A21: ( C = C0 & f . C = the Element of C0 ) by A8, A19;

e9 in C0 by A19, A21;

then consider e2 being Element of the_Edges_of G such that

A22: ( e9 = e2 & e2 Joins v1,v2,G & e2 in E1 ) by A20, A21;

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

end;

suppose A23:
( v = v2 & w = v1 )
; :: thesis: e9 = e

for x being object holds

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

end;( x in C0 iff x in { e where e is Element of the_Edges_of G : ( e Joins v,w,G & e in E1 ) } )

proof

hence
e9 = e
by A17, A19, A21, TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in C0 iff x in { e where e is Element of the_Edges_of G : ( e Joins v,w,G & e in E1 ) } )

then consider e1 being Element of the_Edges_of G such that

A25: ( x = e1 & e1 Joins v,w,G & e1 in E1 ) ;

e1 Joins v1,v2,G by A23, A25, GLIB_000:14;

hence x in C0 by A20, A21, A25; :: thesis: verum

end;hereby :: thesis: ( x in { e where e is Element of the_Edges_of G : ( e Joins v,w,G & e in E1 ) } implies x in C0 )

assume
x in { e where e is Element of the_Edges_of G : ( e Joins v,w,G & e in E1 ) }
; :: thesis: x in C0assume
x in C0
; :: thesis: x in { e where e is Element of the_Edges_of G : ( e Joins v,w,G & e in E1 ) }

then consider e2 being Element of the_Edges_of G such that

A24: ( x = e2 & e2 Joins v1,v2,G & e2 in E1 ) by A20, A21;

e2 Joins v,w,G by A23, A24, GLIB_000:14;

hence x in { e where e is Element of the_Edges_of G : ( e Joins v,w,G & e in E1 ) } by A24; :: thesis: verum

end;then consider e2 being Element of the_Edges_of G such that

A24: ( x = e2 & e2 Joins v1,v2,G & e2 in E1 ) by A20, A21;

e2 Joins v,w,G by A23, A24, GLIB_000:14;

hence x in { e where e is Element of the_Edges_of G : ( e Joins v,w,G & e in E1 ) } by A24; :: thesis: verum

then consider e1 being Element of the_Edges_of G such that

A25: ( x = e1 & e1 Joins v,w,G & e1 in E1 ) ;

e1 Joins v1,v2,G by A23, A25, GLIB_000:14;

hence x in C0 by A20, A21, A25; :: thesis: verum

take E2 ; :: thesis: E2 c= E1

thus E2 c= E1 by A13; :: thesis: verum