let X be set ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ) ; :: thesis: 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 = { c9 where c9 is Element of G -CycleSet : ( rng c9 c= X & not c9 is empty & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c9 & vs . 1 = v ) ) } by Def12;
let c be Element of X -CycleSet v; :: thesis: ( not c is empty & rng c c= X & v in G -VSet (rng c) )
c in X -CycleSet v ;
then consider c9 being Element of G -CycleSet such that
A2: c = c9 and
A3: rng c9 c= X and
A4: not c9 is empty and
A5: ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c9 & vs . 1 = v ) by A1;
thus not c is empty by A2, A4; :: thesis: ( rng c c= X & v in G -VSet (rng c) )
thus rng c c= X by A2, A3; :: thesis: v in G -VSet (rng c)
reconsider c9 = c9 as Path of G by Def8;
consider vs being FinSequence of the carrier of G such that
A6: vs is_vertex_seq_of c9 and
A7: vs . 1 = v by A5;
len vs = (len c9) + 1 by A6;
then 1 <= len vs by NAT_1:11;
then A8: 1 in dom vs by FINSEQ_3:25;
G -VSet (rng c9) = rng vs by A4, A6, GRAPH_2:31;
hence v in G -VSet (rng c) by A2, A7, A8, FUNCT_1:def 3; :: thesis: verum