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

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