:: deftheorem Def3 defines L[01] TREAL_1:def 3 :
for a, b being Real st a <= b holds
for t1, t2 being Point of (Closed-Interval-TSpace (a,b))
for b₅ being Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (a,b)) holds
( b₅ = L[01] (t1,t2) iff for s being Point of (Closed-Interval-TSpace (0,1)) holds b₅ . s = ((1 - s) * t1) + (s * t2) );