REAL m c= REAL m ;
then reconsider X = REAL m as non empty Subset of (REAL m) ;
for x being Element of REAL m st x in X holds
ex r being Real st
( r > 0 & { y where y is Element of REAL m : |.(y - x).| < r } c= X )
proof
let x be Element of REAL m; :: thesis: ( x in X implies ex r being Real st
( r > 0 & { y where y is Element of REAL m : |.(y - x).| < r } c= X ) )
assume x in X ; :: thesis: ex r being Real st
( r > 0 & { y where y is Element of REAL m : |.(y - x).| < r } c= X )
take r = 1; :: thesis: ( r > 0 & { y where y is Element of REAL m : |.(y - x).| < r } c= X )
thus r > 0 ; :: thesis: { y where y is Element of REAL m : |.(y - x).| < r } c= X
now :: thesis: for z being object st z in { y where y is Element of REAL m : |.(y - x).| < r } holds
z in X
let z be object ; :: thesis: ( z in { y where y is Element of REAL m : |.(y - x).| < r } implies z in X )
assume z in { y where y is Element of REAL m : |.(y - x).| < r } ; :: thesis: z in X
then ex y being Element of REAL m st
( z = y & |.(y - x).| < r ) ;
hence z in X ; :: thesis: verum
end;
hence { y where y is Element of REAL m : |.(y - x).| < r } c= X ; :: thesis: verum
end;
then X is open by PDIFF_7:31;
hence ex b1 being non empty Subset of (REAL m) st b1 is open ; :: thesis: verum