Metamath Proof Explorer


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