:: deftheorem defines Tn2TR GTARSKI2:def 3 :
for n being Nat
for P being POINT of (TarskiEuclidSpace n) holds Tn2TR P = P;