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

end;

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