let N be non empty MetrStruct ; :: thesis: {} N is bounded
take 1 ; :: according to TBSP_1:def 9 :: thesis: ( 0 < 1 & ( for x, y being Point of N st x in {} N & y in {} N holds
dist x,y <= 1 ) )
thus ( 0 < 1 & ( for x, y being Point of N st x in {} N & y in {} N holds
dist x,y <= 1 ) ) ; :: thesis: verum