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