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