set N = { y where y is Point of CNS : ||.(y - x0).|| < 1 } ;
take { y where y is Point of CNS : ||.(y - x0).|| < 1 } ; :: thesis: ( { y where y is Point of CNS : ||.(y - x0).|| < 1 } is Subset of CNS & ex g being Real st
( 0 < g & { y where y is Point of CNS : ||.(y - x0).|| < g } c= { y where y is Point of CNS : ||.(y - x0).|| < 1 } ) )
{ y where y is Point of CNS : ||.(y - x0).|| < 1 } 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).|| < 1 } or x in the carrier of CNS )
assume x in { y where y is Point of CNS : ||.(y - x0).|| < 1 } ; :: thesis: x in the carrier of CNS
then ex y being Point of CNS st
( x = y & ||.(y - x0).|| < 1 ) ;
hence x in the carrier of CNS ; :: thesis: verum

end;

hence ( { y where y is Point of CNS : ||.(y - x0).|| < 1 } is Subset of CNS & ex g being Real st
( 0 < g & { y where y is Point of CNS : ||.(y - x0).|| < g } c= { y where y is Point of CNS : ||.(y - x0).|| < 1 } ) ) ; :: thesis: verum