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 A2: a < b ; :: thesis: Closed-Interval-TSpace a,b is connected

set A = the carrier of (Closed-Interval-TSpace 0 ,1);
A3: the carrier of (Closed-Interval-TSpace 0 ,1) = [#] (Closed-Interval-TSpace 0 ,1) ;
L[01] ((#) a,b),(a,b (#) ) is being_homeomorphism by A2, Th20;
then A4: ( 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;
(L[01] ((#) a,b),(a,b (#) )) .: the carrier of (Closed-Interval-TSpace 0 ,1) = rng (L[01] ((#) a,b),(a,b (#) )) by FUNCT_2:45;
hence Closed-Interval-TSpace a,b is connected by A3, A4, Th22, CONNSP_1:15, TOPMETR:27; :: thesis: verum

end;

suppose A5: 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)} & {((#) a,b)} is connected ) by A5, CONNSP_1:29, TOPMETR:25;
hence Closed-Interval-TSpace a,b is connected by CONNSP_1:28; :: thesis: verum

end;

end;

end;

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