let a, b be Real; :: thesis: ( a <= b implies the carrier of (Closed-Interval-MSpace (a,b)) = [.a,b.] )

assume A1: a <= b ; :: thesis: the carrier of (Closed-Interval-MSpace (a,b)) = [.a,b.]

then reconsider P = [.a,b.] as non empty Subset of RealSpace by XXREAL_1:1;

thus the carrier of (Closed-Interval-MSpace (a,b)) = the carrier of (RealSpace | P) by A1, Def3

.= [.a,b.] by Def2 ; :: thesis: verum

assume A1: a <= b ; :: thesis: the carrier of (Closed-Interval-MSpace (a,b)) = [.a,b.]

then reconsider P = [.a,b.] as non empty Subset of RealSpace by XXREAL_1:1;

thus the carrier of (Closed-Interval-MSpace (a,b)) = the carrier of (RealSpace | P) by A1, Def3

.= [.a,b.] by Def2 ; :: thesis: verum