:: deftheorem defines TarskiEuclidSpace GTARSKI2:def 1 :
for n being Nat holds TarskiEuclidSpace n = the naturally_generated TarskiExtension of Euclid n;