let a, b be real number ; :: thesis: ( a <= b implies Closed-Interval-TSpace a,b is arcwise_connected )
assume a <= b ; :: thesis: Closed-Interval-TSpace a,b is arcwise_connected
then reconsider X = Closed-Interval-TSpace a,b as non empty convex SubSpace of R^1 by Th13;
X is arcwise_connected ;
hence Closed-Interval-TSpace a,b is arcwise_connected ; :: thesis: verum