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