theorem Th55: :: FINTOPO8:55

for A being Subset of FMT_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 ) )