let a, b, r, s be Real; :: 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: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; :: thesis: verum

end;

end;