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:33;
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, Th32;
hence Degree (v,(rng c)) is even ; :: thesis: verum

end;

end;

end;

end;

end;