let n be Element of NAT ; :: thesis: for x, p, q being Point of (TOP-REAL n) st x in halfline (p,q) holds
halfline (p,x) c= halfline (p,q)
let x, p, q be Point of (TOP-REAL n); :: 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 number such that
A1: x = ((1 - R) * p) + (R * q) and
A2: 0 <= R by Th26;
let d be set ; :: 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 (TOP-REAL n) ;
consider r being real number such that
A4: d = ((1 - r) * p) + (r * x) and
A5: 0 <= r by A3, Th26;
set o = r * R;
d = ((1 - r) * p) + ((r * ((1 - R) * p)) + (r * (R * q))) by A1, A4, EUCLID:32
.= (((1 - r) * p) + (r * ((1 - R) * p))) + (r * (R * q)) by EUCLID:26
.= (((1 - r) * p) + ((r * (1 - R)) * p)) + (r * (R * q)) by EUCLID:30
.= (((1 - r) + (r * (1 - R))) * p) + (r * (R * q)) by EUCLID:33
.= ((1 - (r * R)) * p) + ((r * R) * q) by EUCLID:30 ;
hence d in halfline (p,q) by A2, A5, Th26; :: thesis: verum