let a, b be Real; :: thesis: for S being sequence of (Closed-Interval-MSpace (a,b)) st a <= b holds

S is sequence of RealSpace

let S be sequence of (Closed-Interval-MSpace (a,b)); :: thesis: ( a <= b implies S is sequence of RealSpace )

assume a <= b ; :: thesis: S is sequence of RealSpace

then the carrier of (Closed-Interval-MSpace (a,b)) = [.a,b.] by TOPMETR:10;

then ( dom S = NAT & rng S c= the carrier of RealSpace ) by FUNCT_2:def 1, METRIC_1:def 13, XBOOLE_1:1;

hence S is sequence of RealSpace by FUNCT_2:2; :: thesis: verum

S is sequence of RealSpace

let S be sequence of (Closed-Interval-MSpace (a,b)); :: thesis: ( a <= b implies S is sequence of RealSpace )

assume a <= b ; :: thesis: S is sequence of RealSpace

then the carrier of (Closed-Interval-MSpace (a,b)) = [.a,b.] by TOPMETR:10;

then ( dom S = NAT & rng S c= the carrier of RealSpace ) by FUNCT_2:def 1, METRIC_1:def 13, XBOOLE_1:1;

hence S is sequence of RealSpace by FUNCT_2:2; :: thesis: verum