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