now :: thesis: for r being Element of REAL st r in [#] REAL holds
ex N being Neighbourhood of r st N c= [#] REAL

let r be Element of REAL ; :: thesis: ( r in [#] REAL implies ex N being Neighbourhood of r st N c= [#] REAL )
assume r in [#] REAL ; :: thesis: ex N being Neighbourhood of r st N c= [#] REAL
].(r - 1),(r + 1).[ is Neighbourhood of r by RCOMP_1:def 6;
hence ex N being Neighbourhood of r st N c= [#] REAL ; :: thesis: verum

end;

hence [#] REAL is open by RCOMP_1:20; :: thesis: verum