Theorem chsh

Description: A closed subspace is a subspace. (Contributed by NM, 19-Oct-1999) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	chsh	⊢ ( 𝐻 ∈ Cℋ → 𝐻 ∈ Sℋ )

Proof

Step	Hyp	Ref	Expression
1		isch	⊢ ( 𝐻 ∈ Cℋ ↔ ( 𝐻 ∈ Sℋ ∧ ( ⇝𝑣 “ ( 𝐻 ↑m ℕ ) ) ⊆ 𝐻 ) )
2	1	simplbi	⊢ ( 𝐻 ∈ Cℋ → 𝐻 ∈ Sℋ )