reconsider P = [.a,b.] as Subset of by METRIC_1:def 14;
reconsider P = P as non empty Subset of by A1, XXREAL_1:1;
take RealSpace | P ; :: thesis: for P being non empty Subset of st P = [.a,b.] holds
RealSpace | P = RealSpace | P
thus for P being non empty Subset of st P = [.a,b.] holds
RealSpace | P = RealSpace | P ; :: thesis: verum