let a, c, d be Real; :: thesis: 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); :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum