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 .first() = W .last() ) by Def24;
then ( W is closed iff (W .reverse() ) .last() = W .last() ) by Th23;
then ( W is closed iff (W .reverse() ) .last() = (W .reverse() ) .first() ) by Th23;
hence ( W is closed iff W .reverse() is closed ) by Def24; :: thesis: verum