let ra, rb be real number ; :: thesis: ( ra <= rb implies [#] (Closed-Interval-TSpace ra,rb) is connected )
assume ra <= rb ; :: thesis: [#] (Closed-Interval-TSpace ra,rb) is connected
then Closed-Interval-TSpace ra,rb is connected by TREAL_1:23;
hence [#] (Closed-Interval-TSpace ra,rb) is connected by CONNSP_1:28; :: thesis: verum