let n be Nat; for p, p1, p2 being Point of (TOP-REAL n) st p in LSeg (p1,p2) holds
LSeg (p1,p) c= LSeg (p1,p2)
let p, p1, p2 be Point of (TOP-REAL n); ( p in LSeg (p1,p2) implies LSeg (p1,p) c= LSeg (p1,p2) )
assume
p in LSeg (p1,p2)
; LSeg (p1,p) c= LSeg (p1,p2)
then consider r being Real such that
A1:
p = ((1 - r) * p1) + (r * p2)
and
A2:
0 <= r
and
A3:
r <= 1
;
let q be object ; TARSKI:def 3 ( not q in LSeg (p1,p) or q in LSeg (p1,p2) )
assume
q in LSeg (p1,p)
; q in LSeg (p1,p2)
then consider b being Real such that
A4:
q = ((1 - b) * p1) + (b * p)
and
A5:
0 <= b
and
A6:
b <= 1
;
A7: q =
((1 - b) * p1) + ((b * ((1 - r) * p1)) + (b * (r * p2)))
by A1, A4, RLVECT_1:def 5
.=
(((1 - b) * p1) + (b * ((1 - r) * p1))) + (b * (r * p2))
by RLVECT_1:def 3
.=
(((1 - b) * p1) + ((b * (1 - r)) * p1)) + (b * (r * p2))
by RLVECT_1:def 7
.=
(((1 - b) + (b * (1 - r))) * p1) + (b * (r * p2))
by RLVECT_1:def 6
.=
((1 - (b * r)) * p1) + ((b * r) * p2)
by RLVECT_1:def 7
;
b * r <= 1
by A2, A3, A6, XREAL_1:160;
hence
q in LSeg (p1,p2)
by A2, A5, A7; verum