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

( W is closed iff W .reverse() is closed )

let W be Walk of G; :: thesis: ( W is closed iff W .reverse() is closed )

( W is closed iff (W .reverse()) .last() = W .last() ) by Th21;

then ( W is closed iff (W .reverse()) .last() = (W .reverse()) .first() ) by Th21;

hence ( W is closed iff W .reverse() is closed ) ; :: thesis: verum

( W is closed iff W .reverse() is closed )

let W be Walk of G; :: thesis: ( W is closed iff W .reverse() is closed )

( W is closed iff (W .reverse()) .last() = W .last() ) by Th21;

then ( W is closed iff (W .reverse()) .last() = (W .reverse()) .first() ) by Th21;

hence ( W is closed iff W .reverse() is closed ) ; :: thesis: verum