let u, v, w be Element of (TOP-REAL 3); :: thesis: ( u in LSeg (v,w) implies |[(u `1),(u `2)]| in LSeg (|[(v `1),(v `2)]|,|[(w `1),(w `2)]|) )
assume u in LSeg (v,w) ; :: thesis: |[(u `1),(u `2)]| in LSeg (|[(v `1),(v `2)]|,|[(w `1),(w `2)]|)
then consider r being Real such that
A1: 0 <= r and
A2: r <= 1 and
A3: u = ((1 - r) * v) + (r * w) by RLTOPSP1:76;
reconsider rv = (1 - r) * v, rw = r * w as Element of (TOP-REAL 3) ;
( rv = |[((1 - r) * (v `1)),((1 - r) * (v `2)),((1 - r) * (v `3))]| & rw = |[(r * (w `1)),(r * (w `2)),(r * (w `3))]| ) by EUCLID_5:7;
then |[(((1 - r) * (v `1)) + (r * (w `1))),(((1 - r) * (v `2)) + (r * (w `2))),(((1 - r) * (v `3)) + (r * (w `3)))]| = u by A3, EUCLID_5:6
.= |[(u `1),(u `2),(u `3)]| by EUCLID_5:3 ;
then A4: ( u `1 = ((1 - r) * (v `1)) + (r * (w `1)) & u `2 = ((1 - r) * (v `2)) + (r * (w `2)) ) by FINSEQ_1:78;
reconsider u9 = |[(u `1),(u `2)]|, v9 = |[(v `1),(v `2)]|, w9 = |[(w `1),(w `2)]| as Element of (TOP-REAL 2) ;
A5: ( u9 `1 = u `1 & u9 `2 = u `2 & v9 `1 = v `1 & v9 `2 = v `2 & w9 `1 = w `1 & w9 `2 = w `2 ) by EUCLID:52;
reconsider rv9 = (1 - r) * v9, rw9 = r * w9 as Element of (TOP-REAL 2) ;
( rv9 = |[((1 - r) * (v9 `1)),((1 - r) * (v9 `2))]| & rw9 = |[(r * (w9 `1)),(r * (w9 `2))]| ) by EUCLID:57;
then rv9 + rw9 = |[(u `1),(u `2)]| by A4, A5, EUCLID:56;
then u9 in { (((1 - r) * v9) + (r * w9)) where r is Real : ( 0 <= r & r <= 1 ) } by A1, A2;
hence |[(u `1),(u `2)]| in LSeg (|[(v `1),(v `2)]|,|[(w `1),(w `2)]|) by RLTOPSP1:def 2; :: thesis: verum