reconsider E = the carrier' of G as finite set by GRAPH_1:def 11;
set XL = { (len p) where p is Element of X -PathSet v : verum } ;
set IT = { c where c is Element of G -CycleSet : ( rng c c= X & not c is empty & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c & vs . 1 = v ) ) } ;
set p = the Element of X -PathSet v;
A3:
len the Element of X -PathSet v in { (len p) where p is Element of X -PathSet v : verum }
;
A4:
{ (len p) where p is Element of X -PathSet v : verum } c= NAT
A5:
X -PathSet v = { c where c is Element of X * : ( c is Path of G & not c is empty & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c & vs . 1 = v ) ) }
by A2, Def11;
{ (len p) where p is Element of X -PathSet v : verum } c= Seg (card E)
then reconsider XL = { (len p) where p is Element of X -PathSet v : verum } as non empty finite Subset of NAT by A3, A4;
set maxl = max XL;
max XL in XL
by XXREAL_2:def 8;
then consider p being Element of X -PathSet v such that
A8:
max XL = len p
;
p in X -PathSet v
;
then consider c being Element of X * such that
A9:
p = c
and
A10:
c is Path of G
and
A11:
not c is empty
and
A12:
ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c & vs . 1 = v )
by A5;
reconsider p = p as Path of G by A9, A10;
A13:
rng c c= X
by FINSEQ_1:def 4;
now p is cyclic set T = the
Target of
G;
set S = the
Source of
G;
A14:
rng p c= X
by A9, FINSEQ_1:def 4;
consider vs being
FinSequence of the
carrier of
G such that A15:
vs is_vertex_seq_of p
and A16:
vs . 1
= v
by A9, A12;
len vs = (len p) + 1
by A15;
then A17:
1
<= len vs
by NAT_1:11;
then
len vs in dom vs
by FINSEQ_3:25;
then reconsider v1 =
vs . (len vs) as
Vertex of
G by FINSEQ_2:11;
assume
not
p is
cyclic
;
contradictionthen A18:
Degree (
v1,
(rng p)) is
odd
by A15, Th50;
then
rng p <> X
by A1;
then
rng p c< X
by A14;
then
ex
xx being
object st
(
xx in X & not
xx in rng p )
by XBOOLE_0:6;
then reconsider Xp =
X \ (rng p) as non
empty set by XBOOLE_0:def 5;
set e = the
Element of
Edges_At (
v1,
Xp);
Degree (
v1,
Xp)
= (Degree (v1,X)) - (Degree (v1,(rng p)))
by A14, Th29;
then
Degree (
v1,
Xp)
<> 0
by A1, A18;
then A19:
not
Edges_At (
v1,
Xp) is
empty
by Th25;
then reconsider ep =
<* the Element of Edges_At (v1,Xp)*> as
Path of
G by Th4;
reconsider t = the
Target of
G . the
Element of
Edges_At (
v1,
Xp),
s = the
Source of
G . the
Element of
Edges_At (
v1,
Xp) as
Vertex of
G by A20, FUNCT_2:5;
then A25:
rng ep misses rng p
by XBOOLE_0:3;
per cases
( v1 = the Target of G . the Element of Edges_At (v1,Xp) or v1 = the Source of G . the Element of Edges_At (v1,Xp) )
by A20;
suppose A26:
v1 = the
Target of
G . the
Element of
Edges_At (
v1,
Xp)
;
contradictionreconsider ts =
<*t,s*> as
FinSequence of the
carrier of
G ;
A27:
vs . (len vs) = ts . 1
by A26;
reconsider X9 =
X as non
empty set by A20;
reconsider vs1 =
vs ^' ts as
FinSequence of the
carrier of
G ;
reconsider e9 = the
Element of
Edges_At (
v1,
Xp) as
Element of
X9 by A20;
A28:
vs1 . 1
= v
by A16, A17, FINSEQ_6:140;
A29:
ts is_vertex_seq_of ep
by Th11;
then reconsider p1 =
p ^ ep as
Path of
G by A15, A25, A27, Th6;
A30:
len p1 =
(len p) + (len ep)
by FINSEQ_1:22
.=
(len p) + 1
by FINSEQ_1:39
;
reconsider p =
p as
FinSequence of
X by A9;
reconsider ep =
<*e9*> as
FinSequence of
X ;
reconsider xp1 =
p ^ ep as
Element of
X * by FINSEQ_1:def 11;
vs1 is_vertex_seq_of p1
by A15, A29, A27, GRAPH_2:44;
then
xp1 in X -PathSet v
by A5, A28;
then reconsider xp1 =
xp1 as
Element of
X -PathSet v ;
len xp1 in XL
;
then
(len p) + 1
<= (len p) + 0
by A8, A30, XXREAL_2:def 8;
hence
contradiction
by XREAL_1:6;
verum end; suppose A31:
v1 = the
Source of
G . the
Element of
Edges_At (
v1,
Xp)
;
contradictionreconsider ts =
<*s,t*> as
FinSequence of the
carrier of
G ;
A32:
(
ts is_vertex_seq_of ep &
vs . (len vs) = ts . 1 )
by A31, MSSCYC_1:4;
then reconsider p1 =
p ^ ep as
Path of
G by A15, A25, Th6;
A33:
len p1 =
(len p) + (len ep)
by FINSEQ_1:22
.=
(len p) + 1
by FINSEQ_1:39
;
reconsider X9 =
X as non
empty set by A20;
reconsider vs1 =
vs ^' ts as
FinSequence of the
carrier of
G ;
reconsider e9 = the
Element of
Edges_At (
v1,
Xp) as
Element of
X9 by A20;
A34:
vs1 . 1
= v
by A16, A17, FINSEQ_6:140;
reconsider p =
p as
FinSequence of
X by A9;
reconsider ep =
<*e9*> as
FinSequence of
X ;
reconsider xp1 =
p ^ ep as
Element of
X * by FINSEQ_1:def 11;
vs1 is_vertex_seq_of p1
by A15, A32, GRAPH_2:44;
then
xp1 in X -PathSet v
by A5, A34;
then reconsider xp1 =
xp1 as
Element of
X -PathSet v ;
len xp1 in XL
;
then
(len p) + 1
<= (len p) + 0
by A8, A33, XXREAL_2:def 8;
hence
contradiction
by XREAL_1:6;
verum end; end;
then reconsider c = c as Element of G -CycleSet by A9, Def8;
c in { c where c is Element of G -CycleSet : ( rng c c= X & not c is empty & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c & vs . 1 = v ) ) }
by A11, A12, A13;
hence
{ c where c is Element of G -CycleSet : ( rng c c= X & not c is empty & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c & vs . 1 = v ) ) } is non empty Subset of (G -CycleSet)
by A35, TARSKI:def 3; verum