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

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 .vertexSeq() ) = 0 ;
then (len W) + 1 = 2 * 0 by Def14;
hence contradiction ; :: thesis: verum

end;

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