let A be Subset of R^1; :: thesis: for a, b being ExtReal st A = ].a,b.[ holds
A is open
let a, b be ExtReal; :: thesis: ( A = ].a,b.[ implies A is open )
].a,b.[ is open by Lm6;
hence ( A = ].a,b.[ implies A is open ) by Th38; :: thesis: verum