:: deftheorem Def13 defines tricord3 EUCLID_3:def 13 :
for n being Element of NAT
for p1, p2, p3, p being Point of (TOP-REAL n) st p2 - p1,p3 - p1 are_lindependent2 & p in plane (p1,p2,p3) holds
for b₆ being Real holds
( b₆ = tricord3 (p1,p2,p3,p) iff ex a1, a2 being Real st
( (a1 + a2) + b₆ = 1 & p = ((a1 * p1) + (a2 * p2)) + (b₆ * p3) ) );