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