theorem :: GLIB_001:80

for G being _Graph
for W being Walk of G ex lenWaa1 being even Element of NAT st
( lenWaa1 = (len W) - 1 & len (W .edgeSeq()) = lenWaa1 div 2 ) by Lm42;