let A, B, C, D be Element of (TOP-REAL 2); :: thesis: ( B in LSeg (A,C) & C in LSeg (A,D) implies B in LSeg (A,D) )
assume that
A1: B in LSeg (A,C) and
A2: C in LSeg (A,D) ; :: thesis: B in LSeg (A,D)
B in { (((1 - r) * A) + (r * C)) where r is Real : ( 0 <= r & r <= 1 ) } by A1, RLTOPSP1:def 2;
then consider r being Real such that
A3: B = ((1 - r) * A) + (r * C) and
A4: 0 <= r and
A5: r <= 1 ;
C in { (((1 - r) * A) + (r * D)) where r is Real : ( 0 <= r & r <= 1 ) } by A2, RLTOPSP1:def 2;
then consider s being Real such that
A6: C = ((1 - s) * A) + (s * D) and
A7: 0 <= s and
A8: s <= 1 ;
reconsider t = r * s as Real ;
A9: r * s <= 1 * 1 by A4, A5, A7, A8, XREAL_1:66;
s * D = |[(s * (D `1)),(s * (D `2))]| by EUCLID:57;
then A10: r * (((1 - s) * A) + (s * D)) = r * (|[((1 - s) * (A `1)),((1 - s) * (A `2))]| + |[(s * (D `1)),(s * (D `2))]|) by EUCLID:57
.= r * |[(((1 - s) * (A `1)) + (s * (D `1))),(((1 - s) * (A `2)) + (s * (D `2)))]| by EUCLID:56
.= |[(r * (((1 - s) * (A `1)) + (s * (D `1)))),(r * (((1 - s) * (A `2)) + (s * (D `2))))]| by EUCLID:58 ;
B = |[((1 - r) * (A `1)),((1 - r) * (A `2))]| + |[(r * (((1 - s) * (A `1)) + (s * (D `1)))),(r * (((1 - s) * (A `2)) + (s * (D `2))))]| by A3, A6, A10, EUCLID:57
.= |[(((1 - r) * (A `1)) + (r * (((1 - s) * (A `1)) + (s * (D `1))))),(((1 - r) * (A `2)) + (r * (((1 - s) * (A `2)) + (s * (D `2)))))]| by EUCLID:56
.= |[(((1 - (r * s)) * (A `1)) + ((r * s) * (D `1))),(((1 - (r * s)) * (A `2)) + ((r * s) * (D `2)))]|
.= |[((1 - (r * s)) * (A `1)),((1 - (r * s)) * (A `2))]| + |[((r * s) * (D `1)),((r * s) * (D `2))]| by EUCLID:56
.= ((1 - (r * s)) * A) + |[((r * s) * (D `1)),((r * s) * (D `2))]| by EUCLID:57
.= ((1 - t) * A) + (t * D) by EUCLID:57 ;
then B in { (((1 - r) * A) + (r * D)) where r is Real : ( 0 <= r & r <= 1 ) } by A9, A4, A7;
hence B in LSeg (A,D) by RLTOPSP1:def 2; :: thesis: verum