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 ) C_ ( Walks ` G )

Proof

Step Hyp Ref Expression
1 clwlkwlk 
 |-  ( w e. ( ClWalks ` G ) -> w e. ( Walks ` G ) )
2 1 ssriv 
 |-  ( ClWalks ` G ) C_ ( Walks ` G )