let G be connected finite Graph; :: thesis: ( ex p being cyclic Path of G st p is Eulerian iff for v being Vertex of G holds Degree v is even )
set E = the carrier' of G;

hereby :: thesis: ( ( for v being Vertex of G holds Degree v is even ) implies ex p being cyclic Path of G st p is Eulerian )

given c being cyclic Path of G such that A1: c is Eulerian ; :: thesis: for v being Vertex of G holds Degree v is even
let v be Vertex of G; :: thesis: Degree v is even
consider vs being FinSequence of the carrier of G such that
A2: vs is_vertex_seq_of c and
vs . 1 = vs . (len vs) by MSSCYC_1:def 2;
rng vs = the carrier of G by A1, A2, Th58;
then A3: Degree (v,(rng c)) is even by A2, Lm4;
rng c = the carrier' of G by A1;
hence Degree v is even by A3, Th24; :: thesis: verum

end;

assume A4: for v being Vertex of G holds Degree v is even ; :: thesis: ex p being cyclic Path of G st p is Eulerian

per cases ( G is void or not G is void ) ;

suppose A5: G is void ; :: thesis: ex p being cyclic Path of G st p is Eulerian

{} is Element of G -CycleSet by Th51;
then reconsider ec = {} as cyclic Path of G by Def8;
take ec ; :: thesis: ec is Eulerian
the carrier' of G is empty by A5;
hence rng ec = the carrier' of G ; :: according to GRAPH_3:def 14 :: thesis: verum

end;

suppose not G is void ; :: thesis: ex p being cyclic Path of G st p is Eulerian

then reconsider G9 = G as non void connected finite Graph ;
reconsider V = the Element of the carrier of G as Vertex of G9 ;
defpred S₁[ Nat, set , set ] means ex E being Element of G9 -CycleSet st
( E = $2 & $3 = ExtendCycle E );
the Element of the carrier' of G -CycleSet V in the carrier' of G -CycleSet V ;
then reconsider ec = the Element of the carrier' of G -CycleSet V as Element of G9 -CycleSet ;
A6: for n being Nat
for x being Element of G9 -CycleSet ex y being Element of G9 -CycleSet st S₁[n,x,y]

proof

let n be Nat; :: thesis: for x being Element of G9 -CycleSet ex y being Element of G9 -CycleSet st S₁[n,x,y]
let x be Element of G9 -CycleSet ; :: thesis: ex y being Element of G9 -CycleSet st S₁[n,x,y]
take ExtendCycle x ; :: thesis: S₁[n,x, ExtendCycle x]
thus S₁[n,x, ExtendCycle x] ; :: thesis: verum

end;

consider f being sequence of (G9 -CycleSet) such that
A7: ( f . 0 = ec & ( for n being Nat holds S₁[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch 2(A6);

A8: now :: thesis: for v being Vertex of G holds Degree (v, the carrier' of G) is even

let v be Vertex of G; :: thesis: Degree (v, the carrier' of G) is even
Degree v = Degree (v, the carrier' of G) by Th24;
hence Degree (v, the carrier' of G) is even by A4; :: thesis: verum

end;

Degree V = Degree (V, the carrier' of G) by Th24;
then A9: Degree (V, the carrier' of G) <> 0 by Th33;

now :: thesis: ex n being Nat ex c being Element of G9 -CycleSet st
( c = f . n & rng c = the carrier' of G )

defpred S₂[ Nat] means ex c being Element of G9 -CycleSet st
( not c is empty & c = f . $1 & $1 <= card (rng c) );
reconsider E = the carrier' of G as finite set by GRAPH_1:def 11;
assume A10: for n being Nat
for c being Element of G9 -CycleSet holds
( not c = f . n or not rng c = the carrier' of G ) ; :: thesis: contradiction
A11: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis: ( S₂[n] implies S₂[n + 1] )
given c being Element of G9 -CycleSet such that A12: not c is empty and
A13: c = f . n and
A14: n <= card (rng c) ; :: thesis: S₂[n + 1]
reconsider r = ExtendCycle c as Element of G9 -CycleSet ;
take r ; :: thesis: ( not r is empty & r = f . (n + 1) & n + 1 <= card (rng r) )
rng c <> E by A10, A13;
hence not r is empty by A4, A12, Th57; :: thesis: ( r = f . (n + 1) & n + 1 <= card (rng r) )
S₁[n,f . n,f . (n + 1)] by A7;
hence r = f . (n + 1) by A13; :: thesis: n + 1 <= card (rng r)
rng c <> E by A10, A13;
then n < card (rng r) by A4, A12, A14, Th57, XXREAL_0:2;
hence n + 1 <= card (rng r) by NAT_1:13; :: thesis: verum

end;

A15: S₂[ 0 ]

proof

take ec ; :: thesis: ( not ec is empty & ec = f . 0 & 0 <= card (rng ec) )
thus not ec is empty by A8, A9, Th55; :: thesis: ( ec = f . 0 & 0 <= card (rng ec) )
thus ec = f . 0 by A7; :: thesis: 0 <= card (rng ec)
thus 0 <= card (rng ec) ; :: thesis: verum

end;

for n being Nat holds S₂[n] from NAT_1:sch 2(A15, A11);
then consider c being Element of G -CycleSet such that
not c is empty and
c = f . ((card E) + 1) and
A16: (card E) + 1 <= card (rng c) ;
rng c c= E by FINSEQ_1:def 4;
then card (rng c) <= card E by NAT_1:43;
then (card E) + 1 <= (card E) + 0 by A16, XXREAL_0:2;
hence contradiction by XREAL_1:6; :: thesis: verum

end;

then consider n being Nat, c being Element of G -CycleSet such that
c = f . n and
A17: rng c = the carrier' of G ;
reconsider c = c as cyclic Path of G by Def8;
take c ; :: thesis: c is Eulerian
thus rng c = the carrier' of G by A17; :: according to GRAPH_3:def 14 :: thesis: verum

end;

end;