let a, b be Real; :: thesis: ( a <= b implies Closed-Interval-TSpace (a,b) is pathwise_connected )
assume a <= b ; :: thesis: Closed-Interval-TSpace (a,b) is pathwise_connected
then reconsider X = Closed-Interval-TSpace (a,b) as non empty interval SubSpace of R^1 by Th9;
X is pathwise_connected ;
hence Closed-Interval-TSpace (a,b) is pathwise_connected ; :: thesis: verum