let a, b be real number ; :: 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 Th13;
X is pathwise_connected ;
hence Closed-Interval-TSpace a,b is pathwise_connected ; :: thesis: verum