reconsider P = [.a,b.] as Subset of RealSpace ;

reconsider P = P as non empty Subset of RealSpace by A1, XXREAL_1:1;

let S1, S2 be non empty strict SubSpace of RealSpace ; :: thesis: ( ( for P being non empty Subset of RealSpace st P = [.a,b.] holds

S1 = RealSpace | P ) & ( for P being non empty Subset of RealSpace st P = [.a,b.] holds

S2 = RealSpace | P ) implies S1 = S2 )

assume that

A2: for P being non empty Subset of RealSpace st P = [.a,b.] holds

S1 = RealSpace | P and

A3: for P being non empty Subset of RealSpace st P = [.a,b.] holds

S2 = RealSpace | P ; :: thesis: S1 = S2

thus S1 = RealSpace | P by A2

.= S2 by A3 ; :: thesis: verum

reconsider P = P as non empty Subset of RealSpace by A1, XXREAL_1:1;

let S1, S2 be non empty strict SubSpace of RealSpace ; :: thesis: ( ( for P being non empty Subset of RealSpace st P = [.a,b.] holds

S1 = RealSpace | P ) & ( for P being non empty Subset of RealSpace st P = [.a,b.] holds

S2 = RealSpace | P ) implies S1 = S2 )

assume that

A2: for P being non empty Subset of RealSpace st P = [.a,b.] holds

S1 = RealSpace | P and

A3: for P being non empty Subset of RealSpace st P = [.a,b.] holds

S2 = RealSpace | P ; :: thesis: S1 = S2

thus S1 = RealSpace | P by A2

.= S2 by A3 ; :: thesis: verum