reconsider P = [.0,1.] as Subset of (TopSpaceMetr RealSpace) by Lm3, METRIC_1:def 13;
A1: I[01] = (TopSpaceMetr RealSpace) | P by Def13;
thus the carrier of I[01] = [#] I[01]
.= [.0,1.] by A1, PRE_TOPC:def 5 ; :: thesis: verum