let A be Subset of R^1; :: thesis: for a being real number st A = ].-infty,a.] holds
A is closed
let a be real number ; :: thesis: ( A = ].-infty,a.] implies A is closed )
assume A1: A = ].-infty,a.] ; :: thesis: A is closed
].-infty,a.] is closed by Lm4;
hence A is closed by A1, TOPREAL6:70; :: thesis: verum