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

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;

hence MetrStruct(# the carrier of M, the distance of M #) is MetrSpace by METRIC_1:6; :: thesis: verum