let a, b, d, e be real number ; :: 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 A1: ( d <= a & a <= b & b <= e & B = [.a,b.] ) ; :: thesis: Closed-Interval-TSpace a,b = (Closed-Interval-TSpace d,e) | B
then A2: d <= b by XXREAL_0:2;
A3: a <= e by A1, XXREAL_0:2;
reconsider A = [.d,e.] as non empty Subset of R^1 by A1, A2, Th24, XXREAL_1:1;
reconsider B2 = [.a,b.] as non empty Subset of R^1 by A1, Th24, XXREAL_1:1;
A4: a in [.d,e.] by A1, A3, XXREAL_1:1;
A5: b in [.d,e.] by A1, A2, XXREAL_1:1;
A6: Closed-Interval-TSpace a,b = R^1 | B2 by A1, Th26;
X: [.a,b.] c= [.d,e.] by A4, A5, XXREAL_2:def 12;
Closed-Interval-TSpace d,e = R^1 | A by A1, A2, Th26, XXREAL_0:2;
hence Closed-Interval-TSpace a,b = (Closed-Interval-TSpace d,e) | B by A1, A6, X, PRE_TOPC:28; :: thesis: verum