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

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