let G be _Graph; :: thesis: for W being Walk of G holds W .cut 1,(len W) = W
let W be Walk of G; :: thesis: W .cut 1,(len W) = W
1 <= len W by HEYTING3:1;
then W .cut 1,(len W) = 1,(len W) -cut W by Def11, JORDAN12:3;
hence W .cut 1,(len W) = W by GRAPH_2:7; :: thesis: verum