reconsider P = [.0 ,1.] as non empty Subset of (TopSpaceMetr RealSpace ) by Lm3, METRIC_1:def 14, XXREAL_1:1;
I[01] = (TopSpaceMetr RealSpace ) | P by Def16;
hence ( I[01] is strict & not I[01] is empty & I[01] is TopSpace-like ) ; :: thesis: verum