let G be _Graph; :: thesis: for W being Walk of G st W .first() <> W .last() & not W .first() ,W .last() are_adjacent holds
W .length() >= 2
let W be Walk of G; :: thesis: ( W .first() <> W .last() & not W .first() ,W .last() are_adjacent implies W .length() >= 2 )
assume that
A1: W .first() <> W .last() and
A2: not W .first() ,W .last() are_adjacent ; :: thesis: W .length() >= 2
set l = W .length() ;
assume W .length() < 2 ; :: thesis: contradiction
then W .length() < 1 + 1 ;
then A3: W .length() <= 1 by NAT_1:13;

per cases ( W .length() = 0 or W .length() = 1 ) by A3, NAT_1:25;

suppose W .length() = 0 ; :: thesis: contradiction

then W is trivial ;
hence contradiction by A1, GLIB_001:127; :: thesis: verum

end;

suppose W .length() = 1 ; :: thesis: contradiction

then A4: len W = (2 * 1) + 1 by GLIB_001:112
.= 3 ;
1 = (2 * 0) + 1 ;
then W . (1 + 1) Joins W . 1,W . (1 + 2),G by A4, GLIB_001:def 3;
hence contradiction by A2, A4; :: thesis: verum

end;

end;