let ra, rb be Real; :: 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:20;
hence [#] (Closed-Interval-TSpace (ra,rb)) is connected by CONNSP_1:27; :: thesis: verum