let a, b be Real; :: 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:18;
hence [#] (Closed-Interval-TSpace (a,b)) is interval ; :: according to TOPALG_2:def 3 :: thesis: verum