let a, b, c be real number ; :: thesis: ( a <= b implies ( c in the carrier of (Closed-Interval-TSpace a,b) iff ( a <= c & c <= b ) ) )
A1: c is Real by XREAL_0:def 1;
assume a <= b ; :: thesis: ( c in the carrier of (Closed-Interval-TSpace a,b) iff ( a <= c & c <= b ) )
then A2: the carrier of (Closed-Interval-TSpace a,b) = [.a,b.] by TOPMETR:25;

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 A2, RCOMP_1:def 1;
then consider c1 being Real such that
A3: ( c1 = c & a <= c1 & c1 <= b ) ;
thus ( a <= c & c <= b ) by A3; :: 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 ) } by A1;
hence c in the carrier of (Closed-Interval-TSpace a,b) by A2, RCOMP_1:def 1; :: thesis: verum