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 A1, JORDAN5A:26
;
set RC = R^1 (right_closed_halfline b);
set LC = R^1 (left_closed_halfline a);
A4:
( R^1 (right_closed_halfline b) = right_closed_halfline b & R^1 (left_closed_halfline a) = left_closed_halfline a )
by TOPREALB:def 3;
then A5:
].a,b.[ ` = (R^1 (left_closed_halfline a)) \/ (R^1 (right_closed_halfline b))
by XXREAL_1:398;
A6:
[.a,b.] /\ ((left_closed_halfline a) \/ (right_closed_halfline b)) = {a,b}
by A1, Th8;
Cl (X `) =
Cl (].a,b.[ `)
by A2, JORDAN5A:24, TOPMETR:17
.=
(Cl (left_closed_halfline a)) \/ (Cl (right_closed_halfline b))
by A4, A5, Th3
.=
(Cl (left_closed_halfline a)) \/ (right_closed_halfline b)
by MEASURE6:59
.=
(left_closed_halfline a) \/ (right_closed_halfline b)
by MEASURE6:59
;
hence
Fr X = {a,b}
by A3, A6, TOPS_1:def 2; verum