let S be RealNormSpace; :: thesis: for x0 being Point of S
for g being Real st 0 < g holds
{ y where y is Point of S : ||.(y - x0).|| < g } is Neighbourhood of x0
let x0 be Point of S; :: thesis: for g being Real st 0 < g holds
{ y where y is Point of S : ||.(y - x0).|| < g } is Neighbourhood of x0
let g be Real; :: thesis: ( 0 < g implies { y where y is Point of S : ||.(y - x0).|| < g } is Neighbourhood of x0 )
assume A1: g > 0 ; :: thesis: { y where y is Point of S : ||.(y - x0).|| < g } is Neighbourhood of x0
set N = { y where y is Point of S : ||.(y - x0).|| < g } ;
{ y where y is Point of S : ||.(y - x0).|| < g } c= the carrier of S

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { y where y is Point of S : ||.(y - x0).|| < g } or x in the carrier of S )
assume x in { y where y is Point of S : ||.(y - x0).|| < g } ; :: thesis: x in the carrier of S
then ex y being Point of S st
( x = y & ||.(y - x0).|| < g ) ;
hence x in the carrier of S ; :: thesis: verum

end;

hence { y where y is Point of S : ||.(y - x0).|| < g } is Neighbourhood of x0 by A1, Def1; :: thesis: verum