:: deftheorem defines trcmap3 EUCLID_3:def 16 :
for p1, p2, p3 being Point of (TOP-REAL 2)
for b₄ being Function of (TOP-REAL 2),R^1 holds
( b₄ = trcmap3 (p1,p2,p3) iff for p being Point of (TOP-REAL 2) holds b₄ . p = tricord3 (p1,p2,p3,p) );