let a, b be Real; :: thesis: 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; :: thesis: ( a < b & X = ].a,b.] implies Fr X = {a,b} )
assume that
A1: a < b and
A2: X = ].a,b.] ; :: thesis: 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:36;
A4: ].a,b.] ` = (left_closed_halfline a) \/ (right_open_halfline b) by XXREAL_1:399;
set RO = R^1 (right_open_halfline b);
set LC = R^1 (left_closed_halfline a);
A5: R^1 (right_open_halfline b) = right_open_halfline b by TOPREALB:def 3;
A6: 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_closed_halfline a)) \/ (Cl (right_open_halfline b)) by A4, Th3
.= (Cl (R^1 (left_closed_halfline a))) \/ (Cl (right_open_halfline b)) by A6, JORDAN5A:24
.= (Cl (R^1 (left_closed_halfline a))) \/ (Cl (R^1 (right_open_halfline b))) by A5, JORDAN5A:24
.= (R^1 (left_closed_halfline a)) \/ (Cl (R^1 (right_open_halfline b))) by PRE_TOPC:22
.= (left_closed_halfline a) \/ (right_closed_halfline b) by A6, BORSUK_5:49, TOPREALB:def 3 ;
hence Fr X = {a,b} by A3, TOPS_1:def 2; :: thesis: verum