reconsider P = [.0 ,1.] as non empty Subset of (TopSpaceMetr RealSpace ) by Lm3, METRIC_1:def 14, XXREAL_1:1;
take (TopSpaceMetr RealSpace ) | P ; :: thesis: for P being Subset of (TopSpaceMetr RealSpace ) st P = [.0 ,1.] holds
(TopSpaceMetr RealSpace ) | P = (TopSpaceMetr RealSpace ) | P
thus for P being Subset of (TopSpaceMetr RealSpace ) st P = [.0 ,1.] holds
(TopSpaceMetr RealSpace ) | P = (TopSpaceMetr RealSpace ) | P ; :: thesis: verum