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

( ( 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

A3:
the distance of M is triangle
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;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

proof

A5:
the distance of M is discerning
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;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

proof

the distance of M is Reflexive
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;assume the distance of M . (a,b) = 0 ; :: thesis: a = b

then dist (a,b) = 0 ;

hence a = b by A1; :: thesis: verum

proof

hence
M is MetrSpace
by A5, A2, A3, Def6, Def7, Def8, Def9; :: thesis: verum
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;the distance of M . (a,a) = dist (a,a)

.= 0 by A1 ;

hence the distance of M . (a,a) = 0 ; :: thesis: verum