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

proof

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

end;

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