set M = MetrStruct(# A,(discrete_dist A) #);
( MetrStruct(# A,(discrete_dist A) #) is Reflexive & MetrStruct(# A,(discrete_dist A) #) is discerning & MetrStruct(# A,(discrete_dist A) #) is symmetric & MetrStruct(# A,(discrete_dist A) #) is triangle )

proof

thus the distance of MetrStruct(# A,(discrete_dist A) #) is Reflexive :: according to METRIC_1:def 7 :: thesis: ( MetrStruct(# A,(discrete_dist A) #) is discerning & MetrStruct(# A,(discrete_dist A) #) is symmetric & MetrStruct(# A,(discrete_dist A) #) is triangle )

proof

let a be Element of MetrStruct(# A,(discrete_dist A) #); :: according to METRIC_1:def 3 :: thesis: the distance of MetrStruct(# A,(discrete_dist A) #) . a,a = 0
thus the distance of MetrStruct(# A,(discrete_dist A) #) . a,a = 0 by Def11; :: thesis: verum

end;

thus the distance of MetrStruct(# A,(discrete_dist A) #) is discerning :: according to METRIC_1:def 8 :: thesis: ( MetrStruct(# A,(discrete_dist A) #) is symmetric & MetrStruct(# A,(discrete_dist A) #) is triangle )

proof

let a, b be Element of MetrStruct(# A,(discrete_dist A) #); :: according to METRIC_1:def 4 :: thesis: ( the distance of MetrStruct(# A,(discrete_dist A) #) . a,b = 0 implies a = b )
assume the distance of MetrStruct(# A,(discrete_dist A) #) . a,b = 0 ; :: thesis: a = b
hence a = b by Def11; :: thesis: verum

end;

thus the distance of MetrStruct(# A,(discrete_dist A) #) is symmetric :: according to METRIC_1:def 9 :: thesis: MetrStruct(# A,(discrete_dist A) #) is triangle

proof

let a, b be Element of MetrStruct(# A,(discrete_dist A) #); :: according to METRIC_1:def 5 :: thesis: the distance of MetrStruct(# A,(discrete_dist A) #) . a,b = the distance of MetrStruct(# A,(discrete_dist A) #) . b,a

now

per cases ( a <> b or a = b ) ;

suppose A1: a <> b ; :: thesis: the distance of MetrStruct(# A,(discrete_dist A) #) . a,b = the distance of MetrStruct(# A,(discrete_dist A) #) . b,a

hence the distance of MetrStruct(# A,(discrete_dist A) #) . a,b = 1 by Def11
.= the distance of MetrStruct(# A,(discrete_dist A) #) . b,a by A1, Def11 ;
:: thesis: verum

end;

suppose a = b ; :: thesis: the distance of MetrStruct(# A,(discrete_dist A) #) . a,b = the distance of MetrStruct(# A,(discrete_dist A) #) . b,a

hence the distance of MetrStruct(# A,(discrete_dist A) #) . a,b = the distance of MetrStruct(# A,(discrete_dist A) #) . b,a ; :: thesis: verum

end;

end;

end;

hence the distance of MetrStruct(# A,(discrete_dist A) #) . a,b = the distance of MetrStruct(# A,(discrete_dist A) #) . b,a ; :: thesis: verum

end;

thus the distance of MetrStruct(# A,(discrete_dist A) #) is triangle :: according to METRIC_1:def 10 :: thesis: verum

proof

let a, b, c be Element of MetrStruct(# A,(discrete_dist A) #); :: according to METRIC_1:def 6 :: thesis: the distance of MetrStruct(# A,(discrete_dist A) #) . a,c <= (the distance of MetrStruct(# A,(discrete_dist A) #) . a,b) + (the distance of MetrStruct(# A,(discrete_dist A) #) . b,c)
A2: ( the distance of MetrStruct(# A,(discrete_dist A) #) . a,b = 0 iff a = b ) by Def11;

per cases ( ( a = b & a = c ) or ( a = b & a <> c ) or ( a = c & a <> b ) or ( b = c & a <> c ) or ( a <> b & a <> c & b <> c ) ) ;

suppose ( a = b & a = c ) ; :: thesis: the distance of MetrStruct(# A,(discrete_dist A) #) . a,c <= (the distance of MetrStruct(# A,(discrete_dist A) #) . a,b) + (the distance of MetrStruct(# A,(discrete_dist A) #) . b,c)

hence the distance of MetrStruct(# A,(discrete_dist A) #) . a,c <= (the distance of MetrStruct(# A,(discrete_dist A) #) . a,b) + (the distance of MetrStruct(# A,(discrete_dist A) #) . b,c) by A2; :: thesis: verum

end;

suppose ( a = b & a <> c ) ; :: thesis: the distance of MetrStruct(# A,(discrete_dist A) #) . a,c <= (the distance of MetrStruct(# A,(discrete_dist A) #) . a,b) + (the distance of MetrStruct(# A,(discrete_dist A) #) . b,c)

hence the distance of MetrStruct(# A,(discrete_dist A) #) . a,c <= (the distance of MetrStruct(# A,(discrete_dist A) #) . a,b) + (the distance of MetrStruct(# A,(discrete_dist A) #) . b,c) by A2; :: thesis: verum

end;

suppose A3: ( a = c & a <> b ) ; :: thesis: the distance of MetrStruct(# A,(discrete_dist A) #) . a,c <= (the distance of MetrStruct(# A,(discrete_dist A) #) . a,b) + (the distance of MetrStruct(# A,(discrete_dist A) #) . b,c)

then A4: the distance of MetrStruct(# A,(discrete_dist A) #) . a,c = 0 by Def11;
A5: the distance of MetrStruct(# A,(discrete_dist A) #) . a,b = 1 by A3, Def11;
the distance of MetrStruct(# A,(discrete_dist A) #) . b,c = 1 by A3, Def11;
hence the distance of MetrStruct(# A,(discrete_dist A) #) . a,c <= (the distance of MetrStruct(# A,(discrete_dist A) #) . a,b) + (the distance of MetrStruct(# A,(discrete_dist A) #) . b,c) by A4, A5; :: thesis: verum

end;

suppose A6: ( b = c & a <> c ) ; :: thesis: the distance of MetrStruct(# A,(discrete_dist A) #) . a,c <= (the distance of MetrStruct(# A,(discrete_dist A) #) . a,b) + (the distance of MetrStruct(# A,(discrete_dist A) #) . b,c)

then the distance of MetrStruct(# A,(discrete_dist A) #) . b,c = 0 by Def11;
hence the distance of MetrStruct(# A,(discrete_dist A) #) . a,c <= (the distance of MetrStruct(# A,(discrete_dist A) #) . a,b) + (the distance of MetrStruct(# A,(discrete_dist A) #) . b,c) by A6; :: thesis: verum

end;

suppose ( a <> b & a <> c & b <> c ) ; :: thesis: the distance of MetrStruct(# A,(discrete_dist A) #) . a,c <= (the distance of MetrStruct(# A,(discrete_dist A) #) . a,b) + (the distance of MetrStruct(# A,(discrete_dist A) #) . b,c)

then ( the distance of MetrStruct(# A,(discrete_dist A) #) . a,c = 1 & the distance of MetrStruct(# A,(discrete_dist A) #) . a,b = 1 & the distance of MetrStruct(# A,(discrete_dist A) #) . b,c = 1 ) by Def11;
hence the distance of MetrStruct(# A,(discrete_dist A) #) . a,c <= (the distance of MetrStruct(# A,(discrete_dist A) #) . a,b) + (the distance of MetrStruct(# A,(discrete_dist A) #) . b,c) ; :: thesis: verum
thus verum ; :: thesis: verum

end;

end;

end;

thus verum ; :: thesis: verum

end;

hence ( DiscreteSpace A is Reflexive & DiscreteSpace A is discerning & DiscreteSpace A is symmetric & DiscreteSpace A is triangle ) ; :: thesis: verum