:: deftheorem Def03 defines length BKMODEL4:def 3 :
for P, Q, R being Point of BK-model-Plane st between P,Q,R & P <> R holds
for b₄ being Real holds
( b₄ = length (P,Q,R) iff ( 0 <= b₄ & b₄ <= 1 & Tn2TR (BK_to_T2 Q) = ((1 - b₄) * (Tn2TR (BK_to_T2 P))) + (b₄ * (Tn2TR (BK_to_T2 R))) ) );