let a, b be real number ; :: thesis: ( a <= b implies the carrier of (Closed-Interval-TSpace a,b) = [.a,b.] )
assume A1: a <= b ; :: thesis: the carrier of (Closed-Interval-TSpace a,b) = [.a,b.]
thus the carrier of (Closed-Interval-TSpace a,b) = the carrier of (Closed-Interval-MSpace a,b) by Th16
.= [.a,b.] by A1, Th14 ; :: thesis: verum