let A be Subset of R^1 ; :: thesis: for a being real number st A = [.a,+infty .[ holds
Int A = ].a,+infty .[
let a be real number ; :: thesis: ( A = [.a,+infty .[ implies Int A = ].a,+infty .[ )
assume A = [.a,+infty .[ ; :: thesis: Int A = ].a,+infty .[
then A ` = ].-infty ,a.[ by TOPMETR:24, XXREAL_1:224, XXREAL_1:294;
then Cl (A ` ) = ].-infty ,a.] by BORSUK_5:77;
then (Cl (A ` )) ` = ].a,+infty .[ by TOPMETR:24, XXREAL_1:224, XXREAL_1:288;
hence Int A = ].a,+infty .[ by TOPS_1:def 1; :: thesis: verum