let G be _Graph; :: thesis: for W being Walk of G holds
( W is Trail-like iff len W = (2 * (card (W .edges()))) + 1 )
let W be Walk of G; :: thesis: ( W is Trail-like iff len W = (2 * (card (W .edges()))) + 1 )
set WE = W .edges() ;
set WES = W .edgeSeq() ;
( W is Trail-like iff (2 * (card (W .edges()))) + 1 = (2 * (len (W .edgeSeq()))) + 1 ) by FINSEQ_4:62;
hence ( W is Trail-like iff len W = (2 * (card (W .edges()))) + 1 ) by GLIB_001:def 15; :: thesis: verum