A1: REAL c= REAL ;

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 Subset of REAL by A1, RCOMP_1:20; :: thesis: verum