let a, b be Real; for X being Subset of R^1 st a <= b & X = [.a,b.] holds
Fr X = {a,b}
let X be Subset of R^1; ( a <= b & X = [.a,b.] implies Fr X = {a,b} )
assume that
A1:
a <= b
and
A2:
X = [.a,b.]
; Fr X = {a,b}
A3: Cl X =
Cl [.a,b.]
by A2, JORDAN5A:24
.=
[.a,b.]
by MEASURE6:59
;
A4:
[.a,b.] /\ ((left_closed_halfline a) \/ (right_closed_halfline b)) = {a,b}
by A1, Th8;
set LO = R^1 (left_open_halfline a);
set RC = R^1 (right_closed_halfline b);
set RO = R^1 (right_open_halfline b);
set LC = R^1 (left_closed_halfline a);
A5:
R^1 (right_closed_halfline b) = right_closed_halfline b
by TOPREALB:def 3;
A6:
R^1 (left_closed_halfline a) = left_closed_halfline a
by TOPREALB:def 3;
A7:
R^1 (right_open_halfline b) = right_open_halfline b
by TOPREALB:def 3;
A8:
R^1 (left_open_halfline a) = left_open_halfline a
by TOPREALB:def 3;
then A9:
[.a,b.] ` = (R^1 (left_open_halfline a)) \/ (R^1 (right_open_halfline b))
by A7, XXREAL_1:385;
Cl (X `) =
Cl ([.a,b.] `)
by A2, JORDAN5A:24, TOPMETR:17
.=
(Cl (left_open_halfline a)) \/ (Cl (right_open_halfline b))
by A8, A7, A9, Th3
.=
(Cl (R^1 (left_open_halfline a))) \/ (Cl (right_open_halfline b))
by A8, JORDAN5A:24
.=
(Cl (R^1 (left_open_halfline a))) \/ (Cl (R^1 (right_open_halfline b)))
by A7, JORDAN5A:24
.=
(R^1 (left_closed_halfline a)) \/ (Cl (R^1 (right_open_halfline b)))
by A6, BORSUK_5:51, TOPREALB:def 3
.=
(R^1 (left_closed_halfline a)) \/ (R^1 (right_closed_halfline b))
by A5, BORSUK_5:49, TOPREALB:def 3
.=
(left_closed_halfline a) \/ (right_closed_halfline b)
by A5, TOPREALB:def 3
;
hence
Fr X = {a,b}
by A3, A4, TOPS_1:def 2; verum