let A be Subset of FMT_R^1; :: thesis: ( A is open iff for x being Real st x in A holds
ex r being Real st
( r > 0 & ].(x - r),(x + r).[ c= A ) )
A is Subset of (NTop2Top (Top2NTop R^1)) by FINTOPO7:def 16;
then reconsider A9 = A as Subset of R^1 by FINTOPO7:24;
hereby :: thesis: ( ( for x being Real st x in A holds
ex r being Real st
( r > 0 & ].(x - r),(x + r).[ c= A ) ) implies A is open )
assume A is open ; :: thesis: for x being Real st x in A holds
ex r being Real st
( r > 0 & ].(x - r),(x + r).[ c= A )
then ( A is open Subset of (NTop2Top FMT_R^1) & NTop2Top FMT_R^1 = R^1 ) by FINTOPO7:24, Lm9;
hence for x being Real st x in A holds
ex r being Real st
( r > 0 & ].(x - r),(x + r).[ c= A ) by FRECHET:8; :: thesis: verum
end;
assume for x being Real st x in A holds
ex r being Real st
( r > 0 & ].(x - r),(x + r).[ c= A ) ; :: thesis: A is open
then A9 is open by FRECHET:8;
hence A is open by Lm1; :: thesis: verum