:: deftheorem defines Tn2R GTARSKI2:def 6 :
for P being POINT of TarskiEuclid2Space holds Tn2R P = P;