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