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;