let n be Element of NAT ; 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); ( x in halfline (p,q) & x <> p implies halfline (p,q) = halfline (p,x) )
assume A1:
x in halfline (p,q)
; ( 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
; halfline (p,q) = halfline (p,x)
thus
halfline (p,q) c= halfline (p,x)
XBOOLE_0:def 10 halfline (p,x) c= halfline (p,q)proof
let d be
set ;
TARSKI:def 3 ( not d in halfline (p,q) or d in halfline (p,x) )
assume A5:
d in halfline (
p,
q)
;
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;
verum
end;
thus
halfline (p,x) c= halfline (p,q)
by A1, Th30; verum