let G be _Graph; :: thesis: for W being Walk of G
for S being Subwalk of W st len S = len W holds
S = W
let W be Walk of G; :: thesis: for S being Subwalk of W st len S = len W holds
S = W
let S be Subwalk of W; :: thesis: ( len S = len W implies S = W )
assume A1: len S = len W ; :: thesis: S = W
A2: len S = (2 * (len (S .edgeSeq()))) + 1 by GLIB_001:def 15;
A3: S .first() = W .first() by GLIB_001:161;
A4: len W = (2 * (len (W .edgeSeq()))) + 1 by GLIB_001:def 15;
ex es being Subset of (W .edgeSeq()) st S .edgeSeq() = Seq es by GLIB_001:def 32;
hence S = W by A1, A2, A4, A3, Th18, Th34; :: thesis: verum