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 9;
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, XBOOLE_0:def 8;
then ex xx being set 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, Th61;
consider c9 being Element of G -CycleSet , v being Vertex of G such that
A5: v = choose X and
A6: c9 = choose (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

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, Th29;
( Degree (v,Erc) = (Degree (v,E9)) - (Degree (v,(rng c))) & Degree (v,(rng ccp)) is even ) by A4, Th34, Th54;
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)) = {} by XBOOLE_0:def 7;
Degree (v,Erc) = (Degree (v,E9)) - (Degree (v,(rng c))) by A4, Th34;
then A12: Degree (v,Erc) <> 0 by A8, Th29;
then rng c9 c= the carrier' of G \ (rng c) by A6, A9, Th60;
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 by XBOOLE_0:def 7;
v in G -VSet (rng c9) by A6, A9, A12, Th60;
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, Th58; :: thesis: card (rng c) < card (rng (ExtendCycle c))
consider vr being Vertex of G such that
A15: vr = choose ((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, XBOOLE_0:def 7;
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:44;
then A19: card (rng (ExtendCycle c)) = (card (rng c)) + (card (rng c9)) by A13, CARD_2:53;
not c9 is empty by A6, A9, A12, Th60;
hence card (rng c) < card (rng (ExtendCycle c)) by A19, XREAL_1:31; :: thesis: verum