let a, b, d, e be Real; :: thesis: for B being Subset of (Closed-Interval-TSpace (d,e)) st d <= a & a <= b & b <= e & B = [.a,b.] holds

Closed-Interval-TSpace (a,b) = (Closed-Interval-TSpace (d,e)) | B

let B be Subset of (Closed-Interval-TSpace (d,e)); :: thesis: ( d <= a & a <= b & b <= e & B = [.a,b.] implies Closed-Interval-TSpace (a,b) = (Closed-Interval-TSpace (d,e)) | B )

assume that

A1: d <= a and

A2: a <= b and

A3: b <= e and

A4: B = [.a,b.] ; :: thesis: Closed-Interval-TSpace (a,b) = (Closed-Interval-TSpace (d,e)) | B

a <= e by A2, A3, XXREAL_0:2;

then A5: a in [.d,e.] by A1, XXREAL_1:1;

A6: d <= b by A1, A2, XXREAL_0:2;

then reconsider A = [.d,e.] as non empty Subset of R^1 by A3, XXREAL_1:1;

b in [.d,e.] by A3, A6, XXREAL_1:1;

then A7: [.a,b.] c= [.d,e.] by A5, XXREAL_2:def 12;

reconsider B2 = [.a,b.] as non empty Subset of R^1 by A2, XXREAL_1:1;

A8: Closed-Interval-TSpace (a,b) = R^1 | B2 by A2, Th19;

Closed-Interval-TSpace (d,e) = R^1 | A by A3, A6, Th19, XXREAL_0:2;

hence Closed-Interval-TSpace (a,b) = (Closed-Interval-TSpace (d,e)) | B by A4, A8, A7, PRE_TOPC:7; :: thesis: verum

Closed-Interval-TSpace (a,b) = (Closed-Interval-TSpace (d,e)) | B

let B be Subset of (Closed-Interval-TSpace (d,e)); :: thesis: ( d <= a & a <= b & b <= e & B = [.a,b.] implies Closed-Interval-TSpace (a,b) = (Closed-Interval-TSpace (d,e)) | B )

assume that

A1: d <= a and

A2: a <= b and

A3: b <= e and

A4: B = [.a,b.] ; :: thesis: Closed-Interval-TSpace (a,b) = (Closed-Interval-TSpace (d,e)) | B

a <= e by A2, A3, XXREAL_0:2;

then A5: a in [.d,e.] by A1, XXREAL_1:1;

A6: d <= b by A1, A2, XXREAL_0:2;

then reconsider A = [.d,e.] as non empty Subset of R^1 by A3, XXREAL_1:1;

b in [.d,e.] by A3, A6, XXREAL_1:1;

then A7: [.a,b.] c= [.d,e.] by A5, XXREAL_2:def 12;

reconsider B2 = [.a,b.] as non empty Subset of R^1 by A2, XXREAL_1:1;

A8: Closed-Interval-TSpace (a,b) = R^1 | B2 by A2, Th19;

Closed-Interval-TSpace (d,e) = R^1 | A by A3, A6, Th19, XXREAL_0:2;

hence Closed-Interval-TSpace (a,b) = (Closed-Interval-TSpace (d,e)) | B by A4, A8, A7, PRE_TOPC:7; :: thesis: verum