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