let a, b, c, d be Real; :: 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:18;
A5: Closed-Interval-TSpace (c,d) is closed SubSpace of R^1 by A3, Th2;
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:18, 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