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