:: deftheorem Def32 defines Subwalk GLIB_001:def 32 :
for G being _Graph
for W, b₃ being Walk of G holds
( b₃ is Subwalk of W iff ( b₃ is_Walk_from W .first() ,W .last() & ex es being Subset of (W .edgeSeq()) st b₃ .edgeSeq() = Seq es ) );