let G be _Graph; for E1 being RepDEdgeSelection of G ex E2 being RepEdgeSelection of G st E2 c= E1
let E1 be RepDEdgeSelection of G; 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 S1[ 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 } & S1[x,y1] & S1[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 S1[x,y]
proof
let x be
object ;
( 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 S1[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 }
;
ex y being object st S1[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;
consider f being Function such that
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
S1[x,f . x] ) )
from FUNCT_1:sch 2(A1, A2);
for e being object st e in rng f holds
e in E1
proof
let e be
object ;
( e in rng f implies e in E1 )
assume
e in rng f
;
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;
verum
end;
then A13:
rng f c= E1
by TARSKI:def 3;
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
let v,
w,
e0 be
object ;
( 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
;
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
;
( 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;
( 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;
for e9 being object st e9 Joins v,w,G & e9 in E2 holds
e9 = e
let e9 be
object ;
( e9 Joins v,w,G & e9 in E2 implies e9 = e )
assume A18:
(
e9 Joins v,
w,
G &
e9 in E2 )
;
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;
suppose A23:
(
v = v2 &
w = v1 )
;
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 ) } )
proof
let x be
object ;
( x in C0 iff x in { e where e is Element of the_Edges_of G : ( e Joins v,w,G & e in E1 ) } )
hereby ( 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 C0
;
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;
verum
end;
assume
x in { e where e is Element of the_Edges_of G : ( e Joins v,w,G & e in E1 ) }
;
x in C0
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;
verum
end; hence
e9 = e
by A17, A19, A21, TARSKI:2;
verum end; end;
end;
then reconsider E2 = E2 as RepEdgeSelection of G by Def5;
take
E2
; E2 c= E1
thus
E2 c= E1
by A13; verum