let G be finite Graph; :: thesis: for v being Vertex of G
for c being cyclic Path of G holds Degree v,(rng c) is even
let v be Vertex of G; :: thesis: for c being cyclic Path of G holds Degree v,(rng c) is even
let c be cyclic Path of G; :: thesis: Degree v,(rng c) is even

per cases ( c is empty or not c is empty ) ;

suppose c is empty ; :: thesis: Degree v,(rng c) is even

then reconsider rc = rng c as empty set ;
Degree v,rc = 2 * 0 ;
hence Degree v,(rng c) is even ; :: thesis: verum

end;

suppose A1: not c is empty ; :: thesis: Degree v,(rng c) is even

consider vs being FinSequence of the carrier of G such that
A2: vs is_vertex_seq_of c by GRAPH_2:36;
thus Degree v,(rng c) is even :: thesis: verum

proof

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

suppose v in rng vs ; :: thesis: Degree v,(rng c) is even

hence Degree v,(rng c) is even by A2, Lm4; :: thesis: verum

end;

suppose not v in rng vs ; :: thesis: Degree v,(rng c) is even

then Degree v,(rng c) = 2 * 0 by A1, A2, Th37;
hence Degree v,(rng c) is even ; :: thesis: verum

end;

end;

end;

end;

end;