let a, b, r, s be Real; :: thesis: ( r <= s implies for X being Subset of (Closed-Interval-TSpace (r,s)) st X = [.a,b.[ & r < a & b <= s holds
Int X = ].a,b.[ )
set L = Closed-Interval-TSpace (r,s);
set c = (r + a) / 2;
set C1 = R^1 ].((r + a) / 2),b.[;
A1: R^1 ].((r + a) / 2),b.[ = ].((r + a) / 2),b.[ by TOPREALB:def 3;
assume r <= s ; :: thesis: for X being Subset of (Closed-Interval-TSpace (r,s)) st X = [.a,b.[ & r < a & b <= s holds
Int X = ].a,b.[
then A2: the carrier of (Closed-Interval-TSpace (r,s)) = [.r,s.] by TOPMETR:18;
let X be Subset of (Closed-Interval-TSpace (r,s)); :: thesis: ( X = [.a,b.[ & r < a & b <= s implies Int X = ].a,b.[ )
assume that
A3: X = [.a,b.[ and
A4: r < a and
A5: b <= s ; :: thesis: Int X = ].a,b.[
A6: r < (r + a) / 2 by A4, XREAL_1:226;
A7: R^1 ].((r + a) / 2),b.[ c= the carrier of (Closed-Interval-TSpace (r,s))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in R^1 ].((r + a) / 2),b.[ or x in the carrier of (Closed-Interval-TSpace (r,s)) )
assume A8: x in R^1 ].((r + a) / 2),b.[ ; :: thesis: x in the carrier of (Closed-Interval-TSpace (r,s))
then reconsider x = x as Real ;
x < b by A1, A8, XXREAL_1:4;
then A9: x <= s by A5, XXREAL_0:2;
(r + a) / 2 < x by A1, A8, XXREAL_1:4;
then r <= x by A6, XXREAL_0:2;
hence x in the carrier of (Closed-Interval-TSpace (r,s)) by A2, A9, XXREAL_1:1; :: thesis: verum

end;

reconsider A = X as Subset of R^1 by PRE_TOPC:11;
A10: (r + a) / 2 < a by A4, XREAL_1:226;
A c= R^1 ].((r + a) / 2),b.[

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in R^1 ].((r + a) / 2),b.[ )
assume A11: x in A ; :: thesis: x in R^1 ].((r + a) / 2),b.[
then reconsider x = x as Real ;
a <= x by A3, A11, XXREAL_1:3;
then A12: (r + a) / 2 < x by A10, XXREAL_0:2;
x < b by A3, A11, XXREAL_1:3;
hence x in R^1 ].((r + a) / 2),b.[ by A1, A12, XXREAL_1:4; :: thesis: verum

end;

then Int A = Int X by A7, TOPS_3:57;
hence Int X = ].a,b.[ by A3, Th38; :: thesis: verum