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