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