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