let G be connected finite Graph; :: thesis: for c being Element of G -CycleSet st rng c <> the carrier' of G & not c is empty & ( for v being Vertex of G holds Degree v is even ) holds
( not ExtendCycle c is empty & card (rng c) < card (rng (ExtendCycle c)) )
let c be Element of G -CycleSet ; :: thesis: ( rng c <> the carrier' of G & not c is empty & ( for v being Vertex of G holds Degree v is even ) implies ( not ExtendCycle c is empty & card (rng c) < card (rng (ExtendCycle c)) ) )
set E = the carrier' of G;
reconsider E9 = the carrier' of G as finite set by GRAPH_1:def 11;
reconsider ccp = c as cyclic Path of G by Def8;
assume that
A1: rng c <> the carrier' of G and
A2: not c is empty and
A3: for v being Vertex of G holds Degree v is even ; :: thesis: ( not ExtendCycle c is empty & card (rng c) < card (rng (ExtendCycle c)) )
A4: rng c c= the carrier' of G by FINSEQ_1:def 4;
then rng c c< the carrier' of G by A1;
then ex xx being object st
( xx in the carrier' of G & not xx in rng c ) by XBOOLE_0:6;
then reconsider Erc = E9 \ (rng c) as non empty finite set by XBOOLE_0:def 5;
reconsider X = { v9 where v9 is Vertex of G : ( v9 in G -VSet (rng c) & Degree v9 <> Degree (v9,(rng c)) ) } as non empty set by A1, A2, Th56;
consider c9 being Element of G -CycleSet , v being Vertex of G such that
A5: v = the Element of X and
A6: c9 = the Element of Erc -CycleSet v and
A7: ExtendCycle c = CatCycles (c,c9) by A1, A2, Def13;
v in X by A5;
then A8: ex v9 being Vertex of G st
( v = v9 & v9 in G -VSet (rng c) & Degree v9 <> Degree (v9,(rng c)) ) ;

A9: now :: thesis: for v being Vertex of G holds Degree (v,Erc) is even

let v be Vertex of G; :: thesis: Degree (v,Erc) is even
A10: ( Degree v = Degree (v, the carrier' of G) & Degree v is even ) by A3, Th24;
( Degree (v,Erc) = (Degree (v,E9)) - (Degree (v,(rng c))) & Degree (v,(rng ccp)) is even ) by A4, Th29, Th49;
hence Degree (v,Erc) is even by A10; :: thesis: verum

end;

rng c misses the carrier' of G \ (rng c) by XBOOLE_1:79;
then A11: (rng c) /\ ( the carrier' of G \ (rng c)) = {} ;
Degree (v,Erc) = (Degree (v,E9)) - (Degree (v,(rng c))) by A4, Th29;
then A12: Degree (v,Erc) <> 0 by A8, Th24;
then rng c9 c= the carrier' of G \ (rng c) by A6, A9, Th55;
then (rng c) /\ (rng c9) = (rng c) /\ (( the carrier' of G \ (rng c)) /\ (rng c9)) by XBOOLE_1:28
.= {} /\ (rng c9) by A11, XBOOLE_1:16
.= {} ;
then A13: rng c misses rng c9 ;
v in G -VSet (rng c9) by A6, A9, A12, Th55;
then A14: G -VSet (rng c) meets G -VSet (rng c9) by A8, XBOOLE_0:3;
hence not ExtendCycle c is empty by A2, A7, A13, Th53; :: thesis: card (rng c) < card (rng (ExtendCycle c))
consider vr being Vertex of G such that
A15: vr = the Element of (G -VSet (rng c)) /\ (G -VSet (rng c9)) and
A16: CatCycles (c,c9) = (Rotate (c,vr)) ^ (Rotate (c9,vr)) by A14, A13, Def10;
A17: (G -VSet (rng c)) /\ (G -VSet (rng c9)) <> {} by A14;
then vr in G -VSet (rng c9) by A15, XBOOLE_0:def 4;
then A18: rng (Rotate (c9,vr)) = rng c9 by Lm5;
vr in G -VSet (rng c) by A17, A15, XBOOLE_0:def 4;
then rng (Rotate (c,vr)) = rng c by Lm5;
then rng (ExtendCycle c) = (rng c) \/ (rng c9) by A7, A16, A18, FINSEQ_1:31;
then A19: card (rng (ExtendCycle c)) = (card (rng c)) + (card (rng c9)) by A13, CARD_2:40;
not c9 is empty by A6, A9, A12, Th55;
hence card (rng c) < card (rng (ExtendCycle c)) by A19, XREAL_1:29; :: thesis: verum