:: deftheorem defines Tn2E GTARSKI2:def 5 :
for P being POINT of TarskiEuclid2Space holds Tn2E P = P;