let V be RealLinearSpace; :: thesis: 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; :: thesis: ( x in halfline (p,q) implies halfline (p,x) c= halfline (p,q) )
assume x in halfline (p,q) ; :: thesis: 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 ; :: according to TARSKI:def 3 :: thesis: ( not d in halfline (p,x) or d in halfline (p,q) )
assume A3: d in halfline (p,x) ; :: thesis: 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; :: thesis: verum