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