Metamath Proof Explorer


Theorem clwlkswks

Description: Closed walks are walks (in an undirected graph). (Contributed by Alexander van der Vekens, 25-Aug-2018) (Revised by AV, 16-Feb-2021)

Ref Expression
Assertion clwlkswks ClWalks G Walks G

Proof

Step Hyp Ref Expression
1 clwlkwlk w ClWalks G w Walks G
2 1 ssriv ClWalks G Walks G