Theorem iiuni

Description: The base set of the unit interval. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 15-Jan-2014)

	Ref	Expression
Assertion	iiuni	⊢ ( 0 [,] 1 ) = ∪ II

Proof

Step	Hyp	Ref	Expression
1		iitopon	⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
2	1	toponunii	⊢ ( 0 [,] 1 ) = ∪ II