let a, b be real number ; :: 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 A1: a <= b ; :: thesis: S is sequence of RealSpace
A2: dom S = NAT by FUNCT_2:def 1;
the carrier of (Closed-Interval-MSpace a,b) = [.a,b.] by A1, TOPMETR:14;
then rng S c= the carrier of RealSpace by METRIC_1:def 14, XBOOLE_1:1;
hence S is sequence of RealSpace by A2, FUNCT_2:4; :: thesis: verum