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

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