MetrStruct(# the carrier of the naturally_generated TarskiExtension of the non empty trivial MetrSpace, the distance of the naturally_generated TarskiExtension of the non empty trivial MetrSpace #) = MetrStruct(# the carrier of the non empty trivial MetrSpace, the distance of the non empty trivial MetrSpace #) by TADef;
hence ( TrivialTarskiSpace is trivial & not TrivialTarskiSpace is empty ) ; :: thesis: verum