theorem :: FRECHET:8

for A being Subset of R^1 holds
( 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 ) )