let G be _Graph; :: thesis: for W being Walk of G
for e, x being set 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 set st e Joins W .last() ,x,G holds
not W .addEdge e is trivial
let e, x be set ; :: thesis: ( e Joins W .last() ,x,G implies not W .addEdge e is trivial )
A1: 1 + 0 < (len W) + 2 by XREAL_1:10;
assume e Joins W .last() ,x,G ; :: thesis: not W .addEdge e is trivial
then len (W .addEdge e) = (len W) + 2 by Lm37;
hence not W .addEdge e is trivial by A1, Lm55; :: thesis: verum