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
A2: the distance of M is symmetric

proof

let a, b be Element of M; :: according to METRIC_1:def 4 :: 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;

A3: the distance of M is triangle

proof

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

end;

A5: the distance of M is discerning

proof

let a, b be Element of M; :: according to METRIC_1:def 3 :: 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;

the distance of M is Reflexive

proof

let a be Element of M; :: according to METRIC_1:def 2 :: 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;

hence M is MetrSpace by A5, A2, A3, Def6, Def7, Def8, Def9; :: thesis: verum