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