let a, c, d be Real; for p being Point of (TOP-REAL 2) st c < d & p `1 = a & c <= p `2 & p `2 <= d holds
p in LSeg (|[a,c]|,|[a,d]|)
let p be Point of (TOP-REAL 2); ( c < d & p `1 = a & c <= p `2 & p `2 <= d implies p in LSeg (|[a,c]|,|[a,d]|) )
assume that
A1:
c < d
and
A2:
p `1 = a
and
A3:
c <= p `2
and
A4:
p `2 <= d
; p in LSeg (|[a,c]|,|[a,d]|)
A5:
d - c > 0
by A1, XREAL_1:50;
reconsider w = ((p `2) - c) / (d - c) as Real ;
A6: ((1 - w) * |[a,c]|) + (w * |[a,d]|) =
|[((1 - w) * a),((1 - w) * c)]| + (w * |[a,d]|)
by EUCLID:58
.=
|[((1 - w) * a),((1 - w) * c)]| + |[(w * a),(w * d)]|
by EUCLID:58
.=
|[(((1 - w) * a) + (w * a)),(((1 - w) * c) + (w * d))]|
by EUCLID:56
.=
|[a,(c + (w * (d - c)))]|
.=
|[a,(c + ((p `2) - c))]|
by A5, XCMPLX_1:87
.=
p
by A2, EUCLID:53
;
A7:
(p `2) - c >= 0
by A3, XREAL_1:48;
(p `2) - c <= d - c
by A4, XREAL_1:9;
then
w <= (d - c) / (d - c)
by A5, XREAL_1:72;
then
w <= 1
by A5, XCMPLX_1:60;
hence
p in LSeg (|[a,c]|,|[a,d]|)
by A5, A6, A7; verum