let T be TarskiExtension of M; :: thesis: not T is empty
MetrStruct(# the carrier of T, the distance of T #) = MetrStruct(# the carrier of M, the distance of M #) by TADef;
hence not T is empty ; :: thesis: verum