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: not 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 not W .addEdge e is trivial by A1, Lm55; :: thesis: verum

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: not 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 not W .addEdge e is trivial by A1, Lm55; :: thesis: verum