let r, s, a, b be real number ; :: 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 = (b + s) / 2;
set C1 = R^1 ].a,((b + s) / 2).[;
A1: R^1 ].a,((b + s) / 2).[ = ].a,((b + s) / 2).[ 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:25;
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: (b + s) / 2 < s by A5, XREAL_1:228;
A7: R^1 ].a,((b + s) / 2).[ c= the carrier of (Closed-Interval-TSpace r,s)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in R^1 ].a,((b + s) / 2).[ or x in the carrier of (Closed-Interval-TSpace r,s) )
assume A8: x in R^1 ].a,((b + s) / 2).[ ; :: thesis: x in the carrier of (Closed-Interval-TSpace r,s)
then reconsider x = x as Real by A1;
x < (b + s) / 2 by A1, A8, XXREAL_1:4;
then A9: x <= s by A6, XXREAL_0:2;
a < x by A1, A8, XXREAL_1:4;
then r <= x by A4, 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:39;
A10: b < (b + s) / 2 by A5, XREAL_1:228;
A c= R^1 ].a,((b + s) / 2).[

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in R^1 ].a,((b + s) / 2).[ )
assume A11: x in A ; :: thesis: x in R^1 ].a,((b + s) / 2).[
then reconsider x = x as Real by A3;
x <= b by A3, A11, XXREAL_1:2;
then A12: x < (b + s) / 2 by A10, XXREAL_0:2;
a < x by A3, A11, XXREAL_1:2;
hence x in R^1 ].a,((b + s) / 2).[ 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, Th51; :: thesis: verum