reconsider P = [.0,1.] as non empty Subset of (TopSpaceMetr RealSpace) by Lm3, METRIC_1:def 13, XXREAL_1:1;

I[01] = (TopSpaceMetr RealSpace) | P by Def13;

hence ( I[01] is strict & not I[01] is empty & I[01] is TopSpace-like ) ; :: thesis: verum

I[01] = (TopSpaceMetr RealSpace) | P by Def13;

hence ( I[01] is strict & not I[01] is empty & I[01] is TopSpace-like ) ; :: thesis: verum