( 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 ; :: thesis: verum