Theorem iitop

Description: The unit interval is a topological space. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Assertion	iitop	⊢ II ∈ Top

Proof

Step	Hyp	Ref	Expression
1		iitopon	⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
2	1	topontopi	⊢ II ∈ Top