let G be _Graph; :: thesis: for W being Walk of G ex lenWaa1 being even Element of NAT st
( lenWaa1 = (len W) - 1 & len (W .edgeSeq()) = lenWaa1 div 2 )
let W be Walk of G; :: thesis: ex lenWaa1 being even Element of NAT st
( lenWaa1 = (len W) - 1 & len (W .edgeSeq()) = lenWaa1 div 2 )
set lenWaa1 = (len W) - 1;
reconsider lenWaa1 = (len W) - 1 as even Element of NAT by ABIAN:12, INT_1:5;
take lenWaa1 ; :: thesis: ( lenWaa1 = (len W) - 1 & len (W .edgeSeq()) = lenWaa1 div 2 )
thus lenWaa1 = (len W) - 1 ; :: thesis: len (W .edgeSeq()) = lenWaa1 div 2
2 divides lenWaa1 by PEPIN:22;
then A1: lenWaa1 = 2 * (lenWaa1 div 2) by NAT_D:3;
len W = (2 * (len (W .edgeSeq()))) + 1 by Def15;
hence len (W .edgeSeq()) = lenWaa1 div 2 by A1; :: thesis: verum