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