let G be _Graph; :: thesis: for W being Walk of G holds W is Subwalk of W

let W be Walk of G; :: thesis: W is Subwalk of W

reconsider es = W .edgeSeq() as Subset of (W .edgeSeq()) by FINSEQ_6:152;

A1: W .edgeSeq() = Seq es by FINSEQ_3:116;

W is_Walk_from W .first() ,W .last() ;

hence W is Subwalk of W by A1, Def32; :: thesis: verum

let W be Walk of G; :: thesis: W is Subwalk of W

reconsider es = W .edgeSeq() as Subset of (W .edgeSeq()) by FINSEQ_6:152;

A1: W .edgeSeq() = Seq es by FINSEQ_3:116;

W is_Walk_from W .first() ,W .last() ;

hence W is Subwalk of W by A1, Def32; :: thesis: verum