let A be Subset of R^1 ; :: thesis: for a being real number st A = ].-infty ,a.[ holds
A is open
let a be real number ; :: thesis: ( A = ].-infty ,a.[ implies A is open )
assume A1: A = ].-infty ,a.[ ; :: thesis: A is open
].-infty ,a.[ is open by Lm8;
hence A is open by A1, Th62; :: thesis: verum