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