let G be _Graph; :: thesis: for W being Walk of G
for x, y being set holds
( W is_Walk_from x,y iff ( W . 1 = x & W . (len W) = y ) )
let W be Walk of G; :: thesis: for x, y being set holds
( W is_Walk_from x,y iff ( W . 1 = x & W . (len W) = y ) )
let x, y be set ; :: thesis: ( W is_Walk_from x,y iff ( W . 1 = x & W . (len W) = y ) )
( W is_Walk_from x,y iff ( W .first() = x & W .last() = y ) ) by Def23;
hence ( W is_Walk_from x,y iff ( W . 1 = x & W . (len W) = y ) ) ; :: thesis: verum