let G be connected finite Graph; 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 ; ( 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 S1[ 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 : S1[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
; { 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 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 A8:
not
v in rng vs
;
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;
verum 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 : S1[v9] } is Subset of the carrier of G
from DOMAIN_1:sch 7();
v in { v9 where v9 is Vertex of G : S1[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; verum