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 Lm7;
hence A is closed by A1, TOPREAL6:79; :: thesis: verum