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