:: deftheorem defines Tarski0Space GTARSKI1:def 20 :
Tarski0Space = the naturally_generated TarskiExtension of ZeroSpace ;