let a, b be real number ; :: 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 = Cl [.a,b.] by A2, TOPREAL6:80
.= [.a,b.] by PSCOMP_1:34 ;
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);
A4: R^1 (left_open_halfline a) = left_open_halfline a by TOPREALB:def 3;
A5: R^1 (right_closed_halfline b) = right_closed_halfline b by TOPREALB:def 3;
A6: R^1 (right_open_halfline b) = right_open_halfline b by TOPREALB:def 3;
A7: R^1 (left_closed_halfline a) = left_closed_halfline a by TOPREALB:def 3;
A8: [.a,b.] ` = (R^1 (left_open_halfline a)) \/ (R^1 (right_open_halfline b)) by A4, A6, XXREAL_1:385;
A9: Cl (X ` ) = Cl ([.a,b.] ` ) by A2, TOPMETR:24, TOPREAL6:80
.= (Cl (left_open_halfline a)) \/ (Cl (right_open_halfline b)) by A4, A6, A8, Th3
.= (Cl (R^1 (left_open_halfline a))) \/ (Cl (right_open_halfline b)) by A4, TOPREAL6:80
.= (Cl (R^1 (left_open_halfline a))) \/ (Cl (R^1 (right_open_halfline b))) by A6, TOPREAL6:80
.= (R^1 (left_closed_halfline a)) \/ (Cl (R^1 (right_open_halfline b))) by A7, BORSUK_5:77, TOPREALB:def 3
.= (R^1 (left_closed_halfline a)) \/ (R^1 (right_closed_halfline b)) by A5, BORSUK_5:75, TOPREALB:def 3
.= (left_closed_halfline a) \/ (right_closed_halfline b) by A5, TOPREALB:def 3 ;
[.a,b.] /\ ((left_closed_halfline a) \/ (right_closed_halfline b)) = {a,b} by A1, Th20;
hence Fr X = {a,b} by A3, A9, TOPS_1:def 2; :: thesis: verum