Theorem 0clwlk0

Description: There is no closed walk in the empty set (i.e. the null graph). (Contributed by Alexander van der Vekens, 2-Sep-2018) (Revised by AV, 5-Mar-2021)

	Ref	Expression
Assertion	0clwlk0	$$⊢\mathrm{ClWalks}\left(\varnothing \right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		clwlkswks	$$⊢\mathrm{ClWalks}\left(\varnothing \right)\subseteq \mathrm{Walks}\left(\varnothing \right)$$
2		0wlk0	$$⊢\mathrm{Walks}\left(\varnothing \right)=\varnothing$$
3		sseq0	$$⊢\left(\mathrm{ClWalks}\left(\varnothing \right)\subseteq \mathrm{Walks}\left(\varnothing \right)\wedge \mathrm{Walks}\left(\varnothing \right)=\varnothing \right)\to \mathrm{ClWalks}\left(\varnothing \right)=\varnothing$$
4	1 2 3	mp2an	$$⊢\mathrm{ClWalks}\left(\varnothing \right)=\varnothing$$