:: deftheorem Def15 defines .edgeSeq() GLIB_001:def 15 :
for G being _Graph
for W being Walk of G
for b₃ being EdgeSeq of G holds
( b₃ = W .edgeSeq() iff ( len W = (2 * (len b₃)) + 1 & ( for n being Nat st 1 <= n & n <= len b₃ holds
b₃ . n = W . (2 * n) ) ) );