let a, b, d be real number ; :: 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 A1: ( a < b & p `2 = d & a <= p `1 & p `1 <= b ) ; :: thesis: p in LSeg |[a,d]|,|[b,d]|
then A2: b - a > 0 by XREAL_1:52;
reconsider w = ((p `1 ) - a) / (b - a) as Real ;
A3: ((1 - w) * |[a,d]|) + (w * |[b,d]|) = |[((1 - w) * a),((1 - w) * d)]| + (w * |[b,d]|) by EUCLID:62
.= |[((1 - w) * a),((1 - w) * d)]| + |[(w * b),(w * d)]| by EUCLID:62
.= |[(((1 - w) * a) + (w * b)),(((1 - w) * d) + (w * d))]| by EUCLID:60
.= |[(a + (w * (b - a))),d]|
.= |[(a + ((p `1 ) - a)),d]| by A2, XCMPLX_1:88
.= p by A1, EUCLID:57 ;
A4: (p `1 ) - a >= 0 by A1, XREAL_1:50;
(p `1 ) - a <= b - a by A1, XREAL_1:11;
then w <= (b - a) / (b - a) by A2, XREAL_1:74;
then ( 0 <= w & w <= 1 ) by A2, A4, XCMPLX_1:60, XREAL_1:138;
then p in { (((1 - lambda) * |[a,d]|) + (lambda * |[b,d]|)) where lambda is Real : ( 0 <= lambda & lambda <= 1 ) } by A3;
hence p in LSeg |[a,d]|,|[b,d]| ; :: thesis: verum