Description: Closed walks are walks (in an undirected graph). (Contributed by Alexander van der Vekens, 23-Jun-2018) (Revised by AV, 16-Feb-2021) (Proof shortened by AV, 30-Oct-2021)