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