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

( 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