let X be set ; for G being finite Graph
for v being Vertex of G st Degree v,X <> 0 & ( for v being Vertex of G holds Degree v,X is even ) holds
for c being Element of X -CycleSet v holds
( not c is empty & rng c c= X & v in G -VSet (rng c) )
let G be finite Graph; for v being Vertex of G st Degree v,X <> 0 & ( for v being Vertex of G holds Degree v,X is even ) holds
for c being Element of X -CycleSet v holds
( not c is empty & rng c c= X & v in G -VSet (rng c) )
let v be Vertex of G; ( Degree v,X <> 0 & ( for v being Vertex of G holds Degree v,X is even ) implies for c being Element of X -CycleSet v holds
( not c is empty & rng c c= X & v in G -VSet (rng c) ) )
assume
( Degree v,X <> 0 & ( for v being Vertex of G holds Degree v,X is even ) )
; for c being Element of X -CycleSet v holds
( not c is empty & rng c c= X & v in G -VSet (rng c) )
then A1:
X -CycleSet v = { c' where c' is Element of G -CycleSet : ( rng c' c= X & not c' is empty & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c' & vs . 1 = v ) ) }
by Def12;
let c be Element of X -CycleSet v; ( not c is empty & rng c c= X & v in G -VSet (rng c) )
c in X -CycleSet v
;
then consider c' being Element of G -CycleSet such that
A2:
c = c'
and
A3:
rng c' c= X
and
A4:
not c' is empty
and
A5:
ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c' & vs . 1 = v )
by A1;
thus
not c is empty
by A2, A4; ( rng c c= X & v in G -VSet (rng c) )
thus
rng c c= X
by A2, A3; v in G -VSet (rng c)
reconsider c' = c' as Path of by Def8;
consider vs being FinSequence of the carrier of G such that
A6:
vs is_vertex_seq_of c'
and
A7:
vs . 1 = v
by A5;
len vs = (len c') + 1
by A6, GRAPH_2:def 7;
then
1 <= len vs
by NAT_1:11;
then A8:
1 in dom vs
by FINSEQ_3:27;
G -VSet (rng c') = rng vs
by A4, A6, GRAPH_2:34;
hence
v in G -VSet (rng c)
by A2, A7, A8, FUNCT_1:def 5; verum