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

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