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