let G be _Graph; :: thesis: for T being Trail of G holds T .length() c= G .size()
let T be Trail of G; :: thesis: T .length() c= G .size()
A1: dom (T .edgeSeq()) = Seg (len (T .edgeSeq())) by FINSEQ_1:def 3
.= Seg (T .length()) by GLIB_001:def 18 ;
( rng (T .edgeSeq()) c= the_Edges_of G & T .edgeSeq() is one-to-one ) by GLIB_001:def 27;
then card (Seg (T .length())) c= card (the_Edges_of G) by A1, CARD_1:10;
then card (T .length()) c= card (the_Edges_of G) by FINSEQ_1:55;
hence T .length() c= G .size() ; :: thesis: verum