set C = the carrier of M;
set R = the Relation of [: the carrier of M, the carrier of M:], the carrier of M;
set E = the Relation of [: the carrier of M, the carrier of M:],[: the carrier of M, the carrier of M:];
take X = MetrTarskiStr(# the carrier of M, the distance of M, the Relation of [: the carrier of M, the carrier of M:], the carrier of M, the Relation of [: the carrier of M, the carrier of M:],[: the carrier of M, the carrier of M:] #); :: thesis: MetrStruct(# the carrier of X, the distance of X #) = MetrStruct(# the carrier of M, the distance of M #)
thus MetrStruct(# the carrier of X, the distance of X #) = MetrStruct(# the carrier of M, the distance of M #) ; :: thesis: verum