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

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