take 2 ; :: according to TBSP_1:def 6 :: thesis: ( 0 < 2 & ( for x, y being Point of (DiscreteSpace A) holds dist (x,y) <= 2 ) )
set N = DiscreteSpace A;
thus 0 < 2 ; :: thesis: for x, y being Point of (DiscreteSpace A) holds dist (x,y) <= 2
let x, y be Point of (DiscreteSpace A); :: thesis: dist (x,y) <= 2
A1: ( DiscreteSpace A = MetrStruct(# A,(discrete_dist A) #) & dist (x,y) = the distance of (DiscreteSpace A) . (x,y) ) by METRIC_1:def 1, METRIC_1:def 11;
( x = y or x <> y ) ;
then ( dist (x,y) = 0 or dist (x,y) = 1 ) by A1, METRIC_1:def 10;
hence dist (x,y) <= 2 ; :: thesis: verum