Theorem cls0

Description: The closure of the empty set. (Contributed by NM, 2-Oct-2007) (Proof shortened by Jim Kingdon, 12-Mar-2023)

	Ref	Expression
Assertion	cls0	$$⊢J\in \mathrm{Top}\to \mathrm{cls}\left(J\right)\left(\varnothing \right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		0cld	$$⊢J\in \mathrm{Top}\to \varnothing \in \mathrm{Clsd}\left(J\right)$$
2		cldcls	$$⊢\varnothing \in \mathrm{Clsd}\left(J\right)\to \mathrm{cls}\left(J\right)\left(\varnothing \right)=\varnothing$$
3	1 2	syl	$$⊢J\in \mathrm{Top}\to \mathrm{cls}\left(J\right)\left(\varnothing \right)=\varnothing$$