:: deftheorem defines Tn2TR GTARSKI2:def 4 :
for P being POINT of TarskiEuclid2Space holds Tn2TR P = P;