:: deftheorem defines TarskiSpace GTARSKI1:def 22 :
TarskiSpace = the naturally_generated TarskiExtension of RealSpace ;