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

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