let V be RealLinearSpace; for p, q, x being Element of V st x in halfline (p,q) holds
halfline (p,x) c= halfline (p,q)
let p, q, x be Element of V; ( x in halfline (p,q) implies halfline (p,x) c= halfline (p,q) )
assume
x in halfline (p,q)
; halfline (p,x) c= halfline (p,q)
then consider R being Real such that
A1:
x = ((1 - R) * p) + (R * q)
and
A2:
0 <= R
;
let d be object ; TARSKI:def 3 ( not d in halfline (p,x) or d in halfline (p,q) )
assume A3:
d in halfline (p,x)
; d in halfline (p,q)
then reconsider d = d as Point of V ;
consider r being Real such that
A4:
d = ((1 - r) * p) + (r * x)
and
A5:
0 <= r
by A3;
set o = r * R;
d =
((1 - r) * p) + ((r * ((1 - R) * p)) + (r * (R * q)))
by A1, A4, RLVECT_1:def 5
.=
(((1 - r) * p) + (r * ((1 - R) * p))) + (r * (R * q))
by RLVECT_1:def 3
.=
(((1 - r) * p) + ((r * (1 - R)) * p)) + (r * (R * q))
by RLVECT_1:def 7
.=
(((1 - r) + (r * (1 - R))) * p) + (r * (R * q))
by RLVECT_1:def 6
.=
((1 - (r * R)) * p) + ((r * R) * q)
by RLVECT_1:def 7
;
hence
d in halfline (p,q)
by A2, A5; verum