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

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