let A be Subset of R^1; :: thesis: for a being Real st A = [.a,+infty.[ holds
A is closed
let a be Real; :: 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, JORDAN5A:23; :: thesis: verum