let a, b be real number ; :: thesis: ( a <= b implies Closed-Interval-TSpace (a,b) is connected )
assume A1: a <= b ; :: thesis: Closed-Interval-TSpace (a,b) is connected

now

per cases ( a < b or a = b ) by A1, XXREAL_0:1;

suppose a < b ; :: thesis: Closed-Interval-TSpace (a,b) is connected

then L[01] (((#) (a,b)),((a,b) (#))) is being_homeomorphism by Th20;
then A2: ( rng (L[01] (((#) (a,b)),((a,b) (#)))) = [#] (Closed-Interval-TSpace (a,b)) & L[01] (((#) (a,b)),((a,b) (#))) is continuous ) by TOPS_2:def 5;
set A = the carrier of (Closed-Interval-TSpace (0,1));
( the carrier of (Closed-Interval-TSpace (0,1)) = [#] (Closed-Interval-TSpace (0,1)) & (L[01] (((#) (a,b)),((a,b) (#)))) .: the carrier of (Closed-Interval-TSpace (0,1)) = rng (L[01] (((#) (a,b)),((a,b) (#)))) ) by FUNCT_2:37;
hence Closed-Interval-TSpace (a,b) is connected by A2, Th22, CONNSP_1:14, TOPMETR:20; :: thesis: verum

end;

suppose A3: a = b ; :: thesis: Closed-Interval-TSpace (a,b) is connected

then ( [.a,b.] = {a} & a = (#) (a,b) ) by Def1, XXREAL_1:17;
then [#] (Closed-Interval-TSpace (a,b)) = {((#) (a,b))} by A3, TOPMETR:18;
hence Closed-Interval-TSpace (a,b) is connected by CONNSP_1:27; :: thesis: verum

end;

end;

end;

hence Closed-Interval-TSpace (a,b) is connected ; :: thesis: verum