let M be MetrSpace; :: thesis: MetrStruct(# the carrier of M, the distance of M #) is MetrSpace

now :: thesis: for a, b, c being Element of MetrStruct(# the carrier of M, the distance 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)) )

hence
MetrStruct(# the carrier of M, the distance of M #) is MetrSpace
by METRIC_1:6; :: thesis: verum( ( 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)) )

let a, b, c be Element of MetrStruct(# the carrier of M, the distance of M #); :: thesis: ( ( 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)) )

reconsider a9 = a, b9 = b, c9 = c as Element of M ;

A1: dist (a,c) = the distance of M . (a,c)

.= dist (a9,c9) ;

A2: dist (a,b) = the distance of M . (a,b)

.= dist (a9,b9) ;

hence ( dist (a,b) = 0 iff a = b ) by METRIC_1:1, METRIC_1:2; :: thesis: ( dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) )

dist (b,a) = the distance of M . (b,a)

.= dist (b9,a9) ;

hence dist (a,b) = dist (b,a) by A2; :: thesis: dist (a,c) <= (dist (a,b)) + (dist (b,c))

dist (b,c) = the distance of M . (b,c)

.= dist (b9,c9) ;

hence dist (a,c) <= (dist (a,b)) + (dist (b,c)) by A2, A1, METRIC_1:4; :: thesis: verum

end;reconsider a9 = a, b9 = b, c9 = c as Element of M ;

A1: dist (a,c) = the distance of M . (a,c)

.= dist (a9,c9) ;

A2: dist (a,b) = the distance of M . (a,b)

.= dist (a9,b9) ;

hence ( dist (a,b) = 0 iff a = b ) by METRIC_1:1, METRIC_1:2; :: thesis: ( dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) )

dist (b,a) = the distance of M . (b,a)

.= dist (b9,a9) ;

hence dist (a,b) = dist (b,a) by A2; :: thesis: dist (a,c) <= (dist (a,b)) + (dist (b,c))

dist (b,c) = the distance of M . (b,c)

.= dist (b9,c9) ;

hence dist (a,c) <= (dist (a,b)) + (dist (b,c)) by A2, A1, METRIC_1:4; :: thesis: verum