let G be _Graph; for E2 being RepEdgeSelection of G ex E1 being RepDEdgeSelection of G st E2 c= E1
let E2 be RepEdgeSelection of G; 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 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 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 ) ) } & 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 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 S1[x,y]
proof
let x be
object ;
( 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 S1[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 ) ) }
;
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 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
;
S1[x, the Element of B]
take
B
;
( x = B & the Element of B = the Element of B )
thus
(
x = B & the
Element of
B = the
Element of
B )
;
verum
end;
consider f being Function such that
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
S1[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
proof
let e be
object ;
( e in rng f implies e in the_Edges_of G )
assume
e in rng f
;
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;
verum
end;
then
rng f c= the_Edges_of G
by TARSKI:def 3;
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
let v,
w,
e0 be
object ;
( 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
;
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;
suppose A14:
e2 DJoins v,
w,
G
;
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
e2
;
( 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;
for e9 being object st e9 DJoins v,w,G & e9 in E1 holds
e9 = e2let e9 be
object ;
( e9 DJoins v,w,G & e9 in E1 implies e9 = e2 )assume A15:
(
e9 DJoins v,
w,
G &
e9 in E1 )
;
e9 = e2
not
e9 in rng f
proof
assume
e9 in rng f
;
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, GLIB_000:125;
hence
contradiction
by A12, A14, A19;
verum
end; then A21:
e9 in E2
by A15, XBOOLE_0:def 3;
e9 Joins v,
w,
G
by A15, GLIB_000:16;
hence
e9 = e2
by A13, A21;
verum end; suppose A22:
(
e2 DJoins w,
v,
G & not
e2 DJoins v,
w,
G )
;
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 ) )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
(
v in the_Vertices_of G &
w in the_Vertices_of G )
by A12, GLIB_000:13;
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
;
( 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;
( 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;
for e9 being object st e9 DJoins v,w,G & e9 in E1 holds
e9 = elet e9 be
object ;
( e9 DJoins v,w,G & e9 in E1 implies e9 = e )assume A28:
(
e9 DJoins v,
w,
G &
e9 in E1 )
;
e9 = e
not
e9 in E2
then
e9 in rng f
by A28, XBOOLE_0:def 3;
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, GLIB_000:125;
hence
e9 = e
by A27, A30, A32;
verum end;
end;
then reconsider E1 = E1 as RepDEdgeSelection of G by Def6;
take
E1
; E2 c= E1
thus
E2 c= E1
by XBOOLE_1:7; verum