let a, b, c be Real; :: thesis: ( a <= b implies ( c in the carrier of (Closed-Interval-TSpace (a,b)) iff ( a <= c & c <= b ) ) )
assume a <= b ; :: thesis: ( c in the carrier of (Closed-Interval-TSpace (a,b)) iff ( a <= c & c <= b ) )
then A1: the carrier of (Closed-Interval-TSpace (a,b)) = [.a,b.] by TOPMETR:18;

hereby :: thesis: ( a <= c & c <= b implies c in the carrier of (Closed-Interval-TSpace (a,b)) )

assume c in the carrier of (Closed-Interval-TSpace (a,b)) ; :: thesis: ( a <= c & c <= b )
then c in { l where l is Real : ( a <= l & l <= b ) } by A1, RCOMP_1:def 1;
then ex c1 being Real st
( c1 = c & a <= c1 & c1 <= b ) ;
hence ( a <= c & c <= b ) ; :: thesis: verum

end;

assume ( a <= c & c <= b ) ; :: thesis: c in the carrier of (Closed-Interval-TSpace (a,b))
then c in { l where l is Real : ( a <= l & l <= b ) } ;
hence c in the carrier of (Closed-Interval-TSpace (a,b)) by A1, RCOMP_1:def 1; :: thesis: verum