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 = [.a,b.] & [.a,b.] /\ ((left_closed_halfline a) \/ (right_closed_halfline b)) = {a,b} )
by A1, A2, Th8, BORSUK_5:35;
set LO = R^1 (left_open_halfline a);
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
by TOPREALB:def 3;
A5:
R^1 (left_open_halfline a) = left_open_halfline a
by TOPREALB:def 3;
then A6:
[.a,b.[ ` = (R^1 (left_open_halfline a)) \/ (R^1 (right_closed_halfline b))
by A4, XXREAL_1:382;
A7:
R^1 (left_closed_halfline a) = left_closed_halfline a
by TOPREALB:def 3;
Cl (X `) =
Cl ([.a,b.[ `)
by A2, JORDAN5A:24, TOPMETR:17
.=
(Cl (left_open_halfline a)) \/ (Cl (right_closed_halfline b))
by A5, A4, A6, Th3
.=
(Cl (R^1 (left_open_halfline a))) \/ (Cl (right_closed_halfline b))
by A5, JORDAN5A:24
.=
(Cl (R^1 (left_open_halfline a))) \/ (Cl (R^1 (right_closed_halfline b)))
by A4, JORDAN5A:24
.=
(R^1 (left_closed_halfline a)) \/ (Cl (R^1 (right_closed_halfline b)))
by A7, BORSUK_5:51, TOPREALB:def 3
.=
(left_closed_halfline a) \/ (right_closed_halfline b)
by A4, A7, PRE_TOPC:22
;
hence
Fr X = {a,b}
by A3, TOPS_1:def 2; verum