let G be _Graph; :: thesis: for W being Walk of G
for e, x being object st e Joins W .last() ,x,G holds
not W .addEdge e is trivial
let W be Walk of G; :: thesis: for e, x being object st e Joins W .last() ,x,G holds
not W .addEdge e is trivial
let e, x be object ; :: thesis: ( e Joins W .last() ,x,G implies not W .addEdge e is trivial )
assume e Joins W .last() ,x,G ; :: thesis: W .addEdge e is trivial
then A1: len (W .addEdge e) = (len W) + 2 by Lm37;
1 + 0 < (len W) + 2 by XREAL_1:8;
hence W .addEdge e is trivial by A1, Lm55; :: thesis: verum