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 Th19
.= I[01] by BORSUK_1:def 13 ; :: thesis: verum