let S be Subset of N; :: thesis: ( S is empty implies S is bounded )
assume A1: S is empty ; :: thesis: S is bounded
take 1 ; :: according to TBSP_1:def 7 :: 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 A1; :: thesis: verum