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

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