reconsider P = [.0 ,1.] as Subset of R^1 ;
set TR = TopSpaceMetr RealSpace ;
reconsider P9 = P as Subset of (TopSpaceMetr RealSpace ) ;
thus Closed-Interval-TSpace 0 ,1 = (TopSpaceMetr RealSpace ) | P9 by Th26
.= I[01] by BORSUK_1:def 16 ; :: thesis: verum