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:65; :: thesis: W .last() = (W .reverse() ) .first()
thus W .last() = (W .reverse() ) .first() by FINSEQ_5:65; :: thesis: verum