let n be Element of NAT ; :: thesis: for x, p, q being Point of (TOP-REAL n) st x in halfline p,q & x <> p holds
halfline p,q = halfline p,x
let x, p, q be Point of (TOP-REAL n); :: thesis: ( x in halfline p,q & x <> p implies halfline p,q = halfline p,x )
assume A1: x in halfline p,q ; :: thesis: ( not x <> p or halfline p,q = halfline p,x )
then consider R being real number such that
A2: x = ((1 - R) * p) + (R * q) and
A3: 0 <= R by Th26;
assume A4: x <> p ; :: thesis: halfline p,q = halfline p,x
thus halfline p,q c= halfline p,x :: according to XBOOLE_0:def 10 :: thesis: halfline p,x c= halfline p,q

proof

let d be set ; :: according to TARSKI:def 3 :: thesis: ( not d in halfline p,q or d in halfline p,x )
assume A5: d in halfline p,q ; :: thesis: d in halfline p,x
then reconsider d = d as Point of (TOP-REAL n) ;
consider r being real number such that
A6: d = ((1 - r) * p) + (r * q) and
A7: 0 <= r by A5, Th26;
set o = r / R;
R <> 0 by A2, A4, Th4;
then (r / R) * R = r by XCMPLX_1:88;
then d = (((1 - (r / R)) + ((r / R) * (1 - R))) * p) + ((r / R) * (R * q)) by A6, EUCLID:34
.= (((1 - (r / R)) * p) + (((r / R) * (1 - R)) * p)) + ((r / R) * (R * q)) by EUCLID:37
.= (((1 - (r / R)) * p) + ((r / R) * ((1 - R) * p))) + ((r / R) * (R * q)) by EUCLID:34
.= ((1 - (r / R)) * p) + (((r / R) * ((1 - R) * p)) + ((r / R) * (R * q))) by EUCLID:30
.= ((1 - (r / R)) * p) + ((r / R) * (((1 - R) * p) + (R * q))) by EUCLID:36 ;
hence d in halfline p,x by A2, A3, A7, Th26; :: thesis: verum

end;

thus halfline p,x c= halfline p,q by A1, Th30; :: thesis: verum