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