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