let a, b, r, s be Real; ( a <= r & s <= b implies [.r,s.] is closed Subset of (Closed-Interval-TSpace (a,b)) )
set T = Closed-Interval-TSpace (a,b);
set A = [.r,s.];
assume that
A1:
a <= r
and
A2:
s <= b
; [.r,s.] is closed Subset of (Closed-Interval-TSpace (a,b))
per cases
( r > s or r <= s )
;
suppose
r <= s
;
[.r,s.] is closed Subset of (Closed-Interval-TSpace (a,b))then
a <= s
by A1, XXREAL_0:2;
then
the
carrier of
(Closed-Interval-TSpace (a,b)) = [.a,b.]
by A2, TOPMETR:18, XXREAL_0:2;
then reconsider A =
[.r,s.] as
Subset of
(Closed-Interval-TSpace (a,b)) by A1, A2, XXREAL_1:34;
reconsider C =
A as
Subset of
R^1 by TOPMETR:17;
(
C is
closed &
C /\ ([#] (Closed-Interval-TSpace (a,b))) = A )
by TREAL_1:1, XBOOLE_1:28;
hence
[.r,s.] is
closed Subset of
(Closed-Interval-TSpace (a,b))
by PRE_TOPC:13;
verum end; end;