let a, b, d, e be Real; 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)); ( 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.]
; 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; verum