let G be connected finite Graph; 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 ; ( 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
; ( 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 for v being Vertex of G holds Degree (v,Erc) is even let v be
Vertex of
G;
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;
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; 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; verum