let G be _Graph; :: thesis: for W being Walk of G st ( len W = 3 or W .length() = 1 ) holds
ex e being object st
( e Joins W .first() ,W .last() ,G & W = G .walkOf ((W .first()),e,(W .last())) )
let W be Walk of G; :: thesis: ( ( len W = 3 or W .length() = 1 ) implies ex e being object st
( e Joins W .first() ,W .last() ,G & W = G .walkOf ((W .first()),e,(W .last())) ) )
assume ( len W = 3 or W .length() = 1 ) ; :: thesis: ex e being object st
( e Joins W .first() ,W .last() ,G & W = G .walkOf ((W .first()),e,(W .last())) )

per cases then ( len W = 3 or W .length() = 1 ) ;

suppose len W = 3 ; :: thesis: ex e being object st
( e Joins W .first() ,W .last() ,G & W = G .walkOf ((W .first()),e,(W .last())) )

hence ex e being object st
( e Joins W .first() ,W .last() ,G & W = G .walkOf ((W .first()),e,(W .last())) ) by Lm2; :: thesis: verum

end;

suppose W .length() = 1 ; :: thesis: ex e being object st
( e Joins W .first() ,W .last() ,G & W = G .walkOf ((W .first()),e,(W .last())) )

then len W = (2 * 1) + 1 by GLIB_001:112;
hence ex e being object st
( e Joins W .first() ,W .last() ,G & W = G .walkOf ((W .first()),e,(W .last())) ) by Lm2; :: thesis: verum

end;

end;