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

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