let G be _Graph; :: thesis: for W being Walk of G holds 1 <= len (W .vertexSeq())
let W be Walk of G; :: thesis: 1 <= len (W .vertexSeq())

now :: thesis: not len (W .vertexSeq()) < 1

assume len (W .vertexSeq()) < 1 ; :: thesis: contradiction
then len (W .vertexSeq()) < 0 + 1 ;
then len (W .vertexSeq()) = 0 by NAT_1:13;
then (len W) + 1 = 2 * 0 by Def14;
hence contradiction ; :: thesis: verum

end;

hence 1 <= len (W .vertexSeq()) ; :: thesis: verum