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:36
.= (((1 - r) * p) + (r * ((1 - R) * p))) + (r * (R * q)) by EUCLID:30
.= (((1 - r) * p) + ((r * (1 - R)) * p)) + (r * (R * q)) by EUCLID:34
.= (((1 - r) + (r * (1 - R))) * p) + (r * (R * q)) by EUCLID:37
.= ((1 - (r * R)) * p) + ((r * R) * q) by EUCLID:34 ;
hence d in halfline p,q by A2, A5, Th26; :: thesis: verum