let a, b be real number ; :: thesis: ( a <= b implies Closed-Interval-TSpace a,b is convex )
set X = Closed-Interval-TSpace a,b;
assume a <= b ; :: thesis: Closed-Interval-TSpace a,b is convex
then [.a,b.] = [#] (Closed-Interval-TSpace a,b) by TOPMETR:25;
hence [#] (Closed-Interval-TSpace a,b) is convex Subset of R^1 by Th8; :: according to TOPALG_2:def 4 :: thesis: verum