let a, c, d be real number ; :: 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:52;
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:62
.= |[((1 - w) * a),((1 - w) * c)]| + |[(w * a),(w * d)]| by EUCLID:62
.= |[(((1 - w) * a) + (w * a)),(((1 - w) * c) + (w * d))]| by EUCLID:60
.= |[a,(c + (w * (d - c)))]|
.= |[a,(c + ((p `2 ) - c))]| by A5, XCMPLX_1:88
.= p by A2, EUCLID:57 ;
A7: (p `2 ) - c >= 0 by A3, XREAL_1:50;
(p `2 ) - c <= d - c by A4, XREAL_1:11;
then w <= (d - c) / (d - c) by A5, XREAL_1:74;
then w <= 1 by A5, XCMPLX_1:60;
hence p in LSeg |[a,c]|,|[a,d]| by A5, A6, A7; :: thesis: verum