for x being Element of REAL 2 st x in [#] (REAL 2) holds
ex r being Real st
( r > 0 & { y where y is Element of REAL 2 : |.(y - x).| < r } c= [#] (REAL 2) )

proof

let x be Element of REAL 2; :: thesis: ( x in [#] (REAL 2) implies ex r being Real st
( r > 0 & { y where y is Element of REAL 2 : |.(y - x).| < r } c= [#] (REAL 2) ) )
assume x in [#] (REAL 2) ; :: thesis: ex r being Real st
( r > 0 & { y where y is Element of REAL 2 : |.(y - x).| < r } c= [#] (REAL 2) )
take 1 ; :: thesis: ( 1 > 0 & { y where y is Element of REAL 2 : |.(y - x).| < 1 } c= [#] (REAL 2) )
thus 0 < 1 ; :: thesis: { y where y is Element of REAL 2 : |.(y - x).| < 1 } c= [#] (REAL 2)

now :: thesis: for s being object st s in { y where y is Element of REAL 2 : |.(y - x).| < 1 } holds
s in [#] (REAL 2)

let s be object ; :: thesis: ( s in { y where y is Element of REAL 2 : |.(y - x).| < 1 } implies s in [#] (REAL 2) )
assume s in { y where y is Element of REAL 2 : |.(y - x).| < 1 } ; :: thesis: s in [#] (REAL 2)
then ex y being Element of REAL 2 st
( s = y & |.(y - x).| < 1 ) ;
hence s in [#] (REAL 2) ; :: thesis: verum

end;

hence { y where y is Element of REAL 2 : |.(y - x).| < 1 } c= [#] (REAL 2) ; :: thesis: verum

end;

hence [#] (REAL 2) is open by PDIFF_7:31; :: thesis: verum