take {} M ; :: thesis: {} M is bounded
take 1 ; :: according to TBSP_1:def 7 :: thesis: ( not 1 <= 0 & ( for b₁, b₂ being Element of the carrier of M holds
( not b₁ in {} M or not b₂ in {} M or dist (b₁,b₂) <= 1 ) ) )
thus ( not 1 <= 0 & ( for b₁, b₂ being Element of the carrier of M holds
( not b₁ in {} M or not b₂ in {} M or dist (b₁,b₂) <= 1 ) ) ) ; :: thesis: verum