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