let V be RealLinearSpace; for p, q, x being Element of V st x in halfline (p,q) & x <> p holds
halfline (p,q) = halfline (p,x)
let p, q, x be Element of V; ( 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 such that
A2:
x = ((1 - R) * p) + (R * q)
and
A3:
0 <= R
;
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
object ;
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
V ;
consider r being
Real such that A6:
d = ((1 - r) * p) + (r * q)
and A7:
0 <= r
by A5;
set o =
r / R;
R <> 0
by A2, A4, Th2;
then
(r / R) * R = r
by XCMPLX_1:87;
then d =
(((1 - (r / R)) + ((r / R) * (1 - R))) * p) + ((r / R) * (R * q))
by A6, RLVECT_1:def 7
.=
(((1 - (r / R)) * p) + (((r / R) * (1 - R)) * p)) + ((r / R) * (R * q))
by RLVECT_1:def 6
.=
(((1 - (r / R)) * p) + ((r / R) * ((1 - R) * p))) + ((r / R) * (R * q))
by RLVECT_1:def 7
.=
((1 - (r / R)) * p) + (((r / R) * ((1 - R) * p)) + ((r / R) * (R * q)))
by RLVECT_1:def 3
.=
((1 - (r / R)) * p) + ((r / R) * (((1 - R) * p) + (R * q)))
by RLVECT_1:def 5
;
hence
d in halfline (
p,
x)
by A2, A3, A7;
verum
end;
thus
halfline (p,x) c= halfline (p,q)
by A1, Th28; verum