( W is closed iff W .first() = W .last() ) by Def24;
then ( W is closed iff (W .reverse() ) .last() = W .last() ) by Lm7;
then ( W is closed iff (W .reverse() ) .last() = (W .reverse() ) .first() ) by Lm7;
hence W .reverse() is closed by Def24; :: thesis: verum