reconsider P2 = BK_to_T2 P, Q2 = BK_to_T2 Q, R2 = BK_to_T2 R as Point of TarskiEuclid2Space ;
reconsider p = P, q = Q, r = R as Element of BK_model ;
( BK_to_T2 P = BK_to_REAL2 p & Tn2TR (BK_to_T2 P) = BK_to_REAL2 p & BK_to_T2 Q = BK_to_REAL2 q & Tn2TR (BK_to_T2 Q) = BK_to_REAL2 q & BK_to_T2 R = BK_to_REAL2 r & Tn2TR (BK_to_T2 R) = BK_to_REAL2 r ) by Th04;
then Tn2TR (BK_to_T2 Q) in LSeg ((Tn2TR (BK_to_T2 P)),(Tn2TR (BK_to_T2 R))) by A1, BKMODEL3:def 7;
then consider r being Real such that
A3: 0 <= r and
A4: r <= 1 and
A5: Tn2TR (BK_to_T2 Q) = ((1 - r) * (Tn2TR (BK_to_T2 P))) + (r * (Tn2TR (BK_to_T2 R))) by RLTOPSP1:76;
take r ; :: thesis: ( 0 <= r & r <= 1 & Tn2TR (BK_to_T2 Q) = ((1 - r) * (Tn2TR (BK_to_T2 P))) + (r * (Tn2TR (BK_to_T2 R))) )
thus ( 0 <= r & r <= 1 & Tn2TR (BK_to_T2 Q) = ((1 - r) * (Tn2TR (BK_to_T2 P))) + (r * (Tn2TR (BK_to_T2 R))) ) by A3, A4, A5; :: thesis: verum