let T be TarskiExtension of M; :: thesis: T is triangle

aa: MetrStruct(# the carrier of T, the distance of T #) = MetrStruct(# the carrier of M, the distance of M #) by TADef;

the distance of M is triangle by METRIC_1:def 9;

hence T is triangle by METRIC_1:def 9, aa; :: thesis: verum

aa: MetrStruct(# the carrier of T, the distance of T #) = MetrStruct(# the carrier of M, the distance of M #) by TADef;

the distance of M is triangle by METRIC_1:def 9;

hence T is triangle by METRIC_1:def 9, aa; :: thesis: verum