take 2 ; :: according to TBSP_1:def 8 :: 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 12;
( x = y or x <> y ) ;
then ( dist x,y = 0 or dist x,y = 1 ) by A1, METRIC_1:def 11;
hence dist x,y <= 2 ; :: thesis: verum