let G be _Graph; :: thesis: for W being Walk of G holds
( W .first() = (W .reverse()) .last() & W .last() = (W .reverse()) .first() )
let W be Walk of G; :: thesis: ( W .first() = (W .reverse()) .last() & W .last() = (W .reverse()) .first() )
len W = len (W .reverse()) by FINSEQ_5:def 3;
hence W .first() = (W .reverse()) .last() by FINSEQ_5:62; :: thesis: W .last() = (W .reverse()) .first()
thus W .last() = (W .reverse()) .first() by FINSEQ_5:62; :: thesis: verum