reconsider P = [.0,1.] as non empty Subset of (TopSpaceMetr RealSpace) by Lm3, METRIC_1:def 13, 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