let n be Nat; for p, q, r being Point of (TOP-REAL n) st q in LSeg (p,r) & r in LSeg (p,q) holds
q = r
let p, q, r be Point of (TOP-REAL n); ( q in LSeg (p,r) & r in LSeg (p,q) implies q = r )
assume
q in LSeg (p,r)
; ( not r in LSeg (p,q) or q = r )
then consider r1 being Real such that
A1:
q = ((1 - r1) * p) + (r1 * r)
and
A2:
0 <= r1
and
A3:
r1 <= 1
;
assume
r in LSeg (p,q)
; q = r
then consider r2 being Real such that
A4:
r = ((1 - r2) * p) + (r2 * q)
and
0 <= r2
and
A5:
r2 <= 1
;
A6:
r1 * r2 <= 1
by A2, A3, A5, XREAL_1:160;
A7:
(1 - r2) + (r2 * (1 - r1)) = 1 - (r2 * r1)
;
A8: r =
((1 - r2) * p) + ((r2 * ((1 - r1) * p)) + (r2 * (r1 * r)))
by A1, A4, RLVECT_1:def 5
.=
(((1 - r2) * p) + (r2 * ((1 - r1) * p))) + (r2 * (r1 * r))
by RLVECT_1:def 3
.=
(((1 - r2) * p) + ((r2 * (1 - r1)) * p)) + (r2 * (r1 * r))
by RLVECT_1:def 7
.=
((1 - (r2 * r1)) * p) + (r2 * (r1 * r))
by A7, RLVECT_1:def 6
.=
((1 - (r2 * r1)) * p) + ((r2 * r1) * r)
by RLVECT_1:def 7
;
A9:
(1 - r1) + (r1 * (1 - r2)) = 1 - (r1 * r2)
;
A10: q =
((1 - r1) * p) + ((r1 * ((1 - r2) * p)) + (r1 * (r2 * q)))
by A1, A4, RLVECT_1:def 5
.=
(((1 - r1) * p) + (r1 * ((1 - r2) * p))) + (r1 * (r2 * q))
by RLVECT_1:def 3
.=
(((1 - r1) * p) + ((r1 * (1 - r2)) * p)) + (r1 * (r2 * q))
by RLVECT_1:def 7
.=
((1 - (r1 * r2)) * p) + (r1 * (r2 * q))
by A9, RLVECT_1:def 6
.=
((1 - (r1 * r2)) * p) + ((r1 * r2) * q)
by RLVECT_1:def 7
;