let G be _Graph; :: thesis: for W being Walk of G holds

( W .first() in W .vertices() & W .last() in W .vertices() )

let W be Walk of G; :: thesis: ( W .first() in W .vertices() & W .last() in W .vertices() )

1 <= len W by ABIAN:12;

hence W .first() in W .vertices() by Lm45, JORDAN12:2; :: thesis: W .last() in W .vertices()

thus W .last() in W .vertices() by Lm45; :: thesis: verum

( W .first() in W .vertices() & W .last() in W .vertices() )

let W be Walk of G; :: thesis: ( W .first() in W .vertices() & W .last() in W .vertices() )

1 <= len W by ABIAN:12;

hence W .first() in W .vertices() by Lm45, JORDAN12:2; :: thesis: W .last() in W .vertices()

thus W .last() in W .vertices() by Lm45; :: thesis: verum