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