let a, r, s, b be real number ; :: thesis: ( 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 ; :: thesis: [.r,s.] is closed Subset of (Closed-Interval-TSpace a,b)

per cases ( r > s or r <= s ) ;

suppose r > s ; :: thesis: [.r,s.] is closed Subset of (Closed-Interval-TSpace a,b)

then [.r,s.] = {} (Closed-Interval-TSpace a,b) by XXREAL_1:29;
hence [.r,s.] is closed Subset of (Closed-Interval-TSpace a,b) ; :: thesis: verum

end;

suppose r <= s ; :: thesis: [.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:25, 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:24;
( C is closed & C /\ ([#] (Closed-Interval-TSpace a,b)) = A ) by TREAL_1:4, XBOOLE_1:28;
hence [.r,s.] is closed Subset of (Closed-Interval-TSpace a,b) by PRE_TOPC:43; :: thesis: verum

end;

end;