let G be _Graph; :: thesis: for P being Path of G holds P .length() c= G .order()
let P be Path of G; :: thesis: P .length() c= G .order()
A1: dom ((P .vertexSeq()) | (P .length())) = Seg (P .length()) by Lm1;
rng ((P .vertexSeq()) | (P .length())) c= the_Vertices_of G ;
then card (Seg (P .length())) c= card (the_Vertices_of G) by A1, CARD_1:10;
then card (P .length()) c= card (the_Vertices_of G) by FINSEQ_1:55;
hence P .length() c= G .order() ; :: thesis: verum