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 A1: ( c < d & p `1 = a & c <= p `2 & p `2 <= d ) ; :: thesis: p in LSeg |[a,c]|,|[a,d]|
then A2: d - c > 0 by XREAL_1:52;
reconsider w = ((p `2 ) - c) / (d - c) as Real ;
A3: ((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 A2, XCMPLX_1:88
.= p by A1, EUCLID:57 ;
A4: (p `2 ) - c >= 0 by A1, XREAL_1:50;
(p `2 ) - c <= d - c by A1, XREAL_1:11;
then w <= (d - c) / (d - c) by A2, XREAL_1:74;
then ( 0 <= w & w <= 1 ) by A2, A4, XCMPLX_1:60;
hence p in LSeg |[a,c]|,|[a,d]| by A3; :: thesis: verum