let a, c, d, b be real number ; :: thesis: ( a <= c & d <= b & c <= d implies Closed-Interval-TSpace c,d is closed SubSpace of Closed-Interval-TSpace a,b )
assume A1: ( a <= c & d <= b & c <= d ) ; :: thesis: Closed-Interval-TSpace c,d is closed SubSpace of Closed-Interval-TSpace a,b
then A2: a <= d by XXREAL_0:2;
[.c,d.] c= [.a,b.] by A1, XXREAL_1:34;
then the carrier of (Closed-Interval-TSpace c,d) c= [.a,b.] by A1, TOPMETR:25;
then A3: the carrier of (Closed-Interval-TSpace c,d) c= the carrier of (Closed-Interval-TSpace a,b) by A1, A2, TOPMETR:25, XXREAL_0:2;
Closed-Interval-TSpace c,d is closed SubSpace of R^1 by A1, Th5;
hence Closed-Interval-TSpace c,d is closed SubSpace of Closed-Interval-TSpace a,b by A3, TSEP_1:14; :: thesis: verum