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, Th63;
then A3: Degree v,(rng c) is even by A2, Lm4;
rng c = the carrier' of G by A1, Def14;
hence Degree v is even by A3, Th29; :: 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 Th56;
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 = choose the carrier of G as Vertex of G9 ;
deffunc H₁( Nat, Element of G9 -CycleSet ) -> Element of G9 -CycleSet = ExtendCycle $2;
choose (the carrier' of G -CycleSet V) in the carrier' of G -CycleSet V ;
then reconsider ec = choose (the carrier' of G -CycleSet V) as Element of G9 -CycleSet ;
consider f being Function of NAT ,(G9 -CycleSet ) such that
A6: ( f . 0 = ec & ( for n being Nat holds f . (n + 1) = H₁(n,f . n) ) ) from NAT_1:sch 12();

A7: now

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

end;

Degree V = Degree V,the carrier' of G by Th29;
then A8: Degree V,the carrier' of G <> 0 by Th38;

now

defpred S₁[ Element of 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 9;
assume A9: for n being Element of NAT
for c being Element of G9 -CycleSet holds
( not c = f . n or not rng c = the carrier' of G ) ; :: thesis: contradiction
A10: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
given c being Element of G9 -CycleSet such that A11: not c is empty and
A12: c = f . n and
A13: 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 A9, A12;
hence not r is empty by A4, A11, Th62; :: thesis: ( r = f . (n + 1) & n + 1 <= card (rng r) )
thus r = f . (n + 1) by A6, A12; :: thesis: n + 1 <= card (rng r)
rng c <> E by A9, A12;
then n < card (rng r) by A4, A11, A13, Th62, XXREAL_0:2;
hence n + 1 <= card (rng r) by NAT_1:13; :: thesis: verum

end;

A14: S₁[ 0 ]

proof

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

end;

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

end;

then consider n being Element of NAT , c being Element of G -CycleSet such that
c = f . n and
A16: 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 A16; :: according to GRAPH_3:def 14 :: thesis: verum

end;

end;