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 that
A1: a <= c and
A2: d <= b and
A3: c <= d ; :: thesis: Closed-Interval-TSpace c,d is closed SubSpace of Closed-Interval-TSpace a,b
[.c,d.] c= [.a,b.] by A1, A2, XXREAL_1:34;
then A4: the carrier of (Closed-Interval-TSpace c,d) c= [.a,b.] by A3, TOPMETR:25;
A5: Closed-Interval-TSpace c,d is closed SubSpace of R^1 by A3, Th5;
a <= d by A1, A3, XXREAL_0:2;
then the carrier of (Closed-Interval-TSpace c,d) c= the carrier of (Closed-Interval-TSpace a,b) by A2, A4, TOPMETR:25, XXREAL_0:2;
hence Closed-Interval-TSpace c,d is closed SubSpace of Closed-Interval-TSpace a,b by A5, TSEP_1:14; :: thesis: verum