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

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