let T be TarskiExtension of M; :: thesis: T is Reflexive
aa: MetrStruct(# the carrier of T, the distance of T #) = MetrStruct(# the carrier of M, the distance of M #) by TADef;
the distance of T is Reflexive by METRIC_1:def 6, aa;
hence T is Reflexive by METRIC_1:def 6; :: thesis: verum