let M be MetrStruct ; :: thesis: ( ( for a, b, c being Element of M holds
( ( dist a,b = 0 implies a = b ) & ( a = b implies dist a,b = 0 ) & dist a,b = dist b,a & dist a,c <= (dist a,b) + (dist b,c) ) ) implies M is MetrSpace )
assume A1: for a, b, c being Element of M holds
( ( dist a,b = 0 implies a = b ) & ( a = b implies dist a,b = 0 ) & dist a,b = dist b,a & dist a,c <= (dist a,b) + (dist b,c) ) ; :: thesis: M is MetrSpace
( M is Reflexive & M is discerning & M is symmetric & M is triangle )

proof

thus the distance of M is Reflexive :: according to METRIC_1:def 7 :: thesis: ( M is discerning & M is symmetric & M is triangle )

proof

let a be Element of M; :: according to METRIC_1:def 3 :: thesis: the distance of M . a,a = 0
the distance of M . a,a = dist a,a
.= 0 by A1 ;
hence the distance of M . a,a = 0 ; :: thesis: verum

end;

thus the distance of M is discerning :: according to METRIC_1:def 8 :: thesis: ( M is symmetric & M is triangle )

proof

let a, b be Element of M; :: according to METRIC_1:def 4 :: thesis: ( the distance of M . a,b = 0 implies a = b )
assume the distance of M . a,b = 0 ; :: thesis: a = b
then dist a,b = 0 ;
hence a = b by A1; :: thesis: verum

end;

thus the distance of M is symmetric :: according to METRIC_1:def 9 :: thesis: M is triangle

proof

let a, b be Element of M; :: according to METRIC_1:def 5 :: thesis: the distance of M . a,b = the distance of M . b,a
the distance of M . a,b = dist a,b
.= dist b,a by A1
.= the distance of M . b,a ;
hence the distance of M . a,b = the distance of M . b,a ; :: thesis: verum

end;

thus the distance of M is triangle :: according to METRIC_1:def 10 :: thesis: verum

proof

let a, b, c be Element of M; :: according to METRIC_1:def 6 :: thesis: the distance of M . a,c <= (the distance of M . a,b) + (the distance of M . b,c)
A2: the distance of M . a,c = dist a,c ;
A3: the distance of M . a,b = dist a,b ;
the distance of M . b,c = dist b,c ;
hence the distance of M . a,c <= (the distance of M . a,b) + (the distance of M . b,c) by A1, A2, A3; :: thesis: verum

end;

end;

hence M is MetrSpace ; :: thesis: verum