:: deftheorem defines TrivialTarskiSpace GTARSKI1:def 16 :
TrivialTarskiSpace = the naturally_generated TarskiExtension of the non empty trivial MetrSpace;