let G be _Graph; :: thesis: for W being Walk of G st len W = 3 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 implies ex e being object st
( e Joins W .first() ,W .last() ,G & W = G .walkOf ((W .first()),e,(W .last())) ) )
assume A1: len W = 3 ; :: thesis: ex e being object st
( e Joins W .first() ,W .last() ,G & W = G .walkOf ((W .first()),e,(W .last())) )
then A2: W . (1 + 1) Joins W . 1,W . (1 + 2),G by GLIB_001:def 3, POLYFORM:4;
take W . 2 ; :: thesis: ( W . 2 Joins W .first() ,W .last() ,G & W = G .walkOf ((W .first()),(W . 2),(W .last())) )
A3: ( W . 1 = W .first() & W . 3 = W .last() ) by A1, GLIB_001:def 6, GLIB_001:def 7;
hence A4: W . 2 Joins W .first() ,W .last() ,G by A2; :: thesis: W = G .walkOf ((W .first()),(W . 2),(W .last()))
thus W = <*(W . 1),(W . 2),(W . 3)*> by A1, FINSEQ_1:45
.= G .walkOf ((W .first()),(W . 2),(W .last())) by A3, A4, GLIB_001:def 5 ; :: thesis: verum