let a, b, r, s be Real; ( 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
; 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)); ( 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
; 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 ;
TARSKI:def 3 ( 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.[
;
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;
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 ;
TARSKI:def 3 ( not x in A or x in R^1 ].((r + a) / 2),b.[ )
assume A11:
x in A
;
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;
verum
end;
then
Int A = Int X
by A7, TOPS_3:57;
hence
Int X = ].a,b.[
by A3, Th38; verum