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 holds
{ v9 where v9 is Vertex of G : ( v9 in G -VSet (rng c) & Degree v9 <> Degree (v9,(rng c)) ) } is non empty Subset of the carrier of G
let c be Element of G -CycleSet ; :: thesis: ( rng c <> the carrier' of G & not c is empty implies { v9 where v9 is Vertex of G : ( v9 in G -VSet (rng c) & Degree v9 <> Degree (v9,(rng c)) ) } is non empty Subset of the carrier of G )
defpred S₁[ Vertex of G] means ( $1 in G -VSet (rng c) & Degree $1 <> Degree ($1,(rng c)) );
set X = { v9 where v9 is Vertex of G : S₁[v9] } ;
set T = the Target of G;
set S = the Source of G;
set E = the carrier' of G;
A1: rng c c= the carrier' of G by FINSEQ_1:def 4;
reconsider cp = c as cyclic Path of G by Def8;
assume that
A2: rng c <> the carrier' of G and
A3: not c is empty ; :: thesis: { v9 where v9 is Vertex of G : ( v9 in G -VSet (rng c) & Degree v9 <> Degree (v9,(rng c)) ) } is non empty Subset of the carrier of G
consider vs being FinSequence of the carrier of G such that
A4: vs is_vertex_seq_of cp by GRAPH_2:33;
A5: G -VSet (rng cp) = rng vs by A3, A4, GRAPH_2:31;

now :: thesis: ex v being Vertex of G st
( v in rng vs & Degree v <> Degree (v,(rng c)) )

consider x being object such that
A6: ( ( x in rng c & not x in the carrier' of G ) or ( x in the carrier' of G & not x in rng c ) ) by A2, TARSKI:2;
reconsider x = x as Element of the carrier' of G by A1, A6;
reconsider v = the Target of G . x as Vertex of G by A1, A6, FUNCT_2:5;

per cases ( v in rng vs or not v in rng vs ) ;

suppose A7: v in rng vs ; :: thesis: ex v being Vertex of G st
( v in rng vs & Degree v <> Degree (v,(rng c)) )

Degree v <> Degree (v,(rng c)) by A1, A6, Th26;
hence ex v being Vertex of G st
( v in rng vs & Degree v <> Degree (v,(rng c)) ) by A7; :: thesis: verum

end;

suppose A8: not v in rng vs ; :: thesis: ex v being Vertex of G st
( v in rng vs & Degree v <> Degree (v,(rng c)) )

A9: ex e being object st e in rng c by A3, XBOOLE_0:def 1;
then rng c meets the carrier' of G by A1, XBOOLE_0:3;
then consider v9 being Vertex of G, e being Element of the carrier' of G such that
A10: v9 in rng vs and
A11: ( not e in rng c & ( v9 = the Target of G . e or v9 = the Source of G . e ) ) by A5, A8, Th19;
Degree v9 <> Degree (v9,(rng c)) by A1, A9, A11, Th26;
hence ex v being Vertex of G st
( v in rng vs & Degree v <> Degree (v,(rng c)) ) by A10; :: thesis: verum

end;

end;

end;

then consider v being Vertex of G such that
A12: ( v in rng vs & Degree v <> Degree (v,(rng c)) ) ;
A13: { v9 where v9 is Vertex of G : S₁[v9] } is Subset of the carrier of G from DOMAIN_1:sch 7();
v in { v9 where v9 is Vertex of G : S₁[v9] } by A5, A12;
hence { v9 where v9 is Vertex of G : ( v9 in G -VSet (rng c) & Degree v9 <> Degree (v9,(rng c)) ) } is non empty Subset of the carrier of G by A13; :: thesis: verum