let G be finite Graph; :: thesis: for ps being oriented Simple Chain of G holds len ps <= EdgesCount G
let ps be oriented Simple Chain of G; :: thesis: len ps <= EdgesCount G
reconsider V = the carrier' of G as finite set ;
rng ps c= the carrier' of G by FINSEQ_1:def 4;
then A1: card (rng ps) <= card V by NAT_1:43;
ps is V18() by Th15;
then card (rng ps) = len ps by FINSEQ_4:62;
hence len ps <= EdgesCount G by A1, GRAPH_1:def 20; :: thesis: verum