let S be Subset of N; :: thesis: ( S is empty implies S is bounded )
assume X: S is empty ; :: thesis: S is bounded
take 1 ; :: according to TBSP_1:def 9 :: thesis: ( 0 < 1 & ( for x, y being Point of N st x in S & y in S holds
dist x,y <= 1 ) )
thus ( 0 < 1 & ( for x, y being Point of N st x in S & y in S holds
dist x,y <= 1 ) ) by X; :: thesis: verum