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

now

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