let u, v, w be Element of (TOP-REAL 2); :: thesis: ( u in LSeg (v,w) implies |[(u `1),(u `2),1]| in LSeg (|[(v `1),(v `2),1]|,|[(w `1),(w `2),1]|) )
assume u in LSeg (v,w) ; :: thesis: |[(u `1),(u `2),1]| in LSeg (|[(v `1),(v `2),1]|,|[(w `1),(w `2),1]|)
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 u9 = |[(u `1),(u `2),1]|, v9 = |[(v `1),(v `2),1]|, w9 = |[(w `1),(w `2),1]| as Element of (TOP-REAL 3) ;
reconsider rv = (1 - r) * v, rw = r * w as Element of REAL 2 by EUCLID:22;
A4: ( rv . 1 = (1 - r) * (v . 1) & rv . 2 = (1 - r) * (v . 2) & rw . 1 = r * (w . 1) & rw . 2 = r * (w . 2) ) by RVSUM_1:44;
A5: u `2 = ((1 - r) * (v . 2)) + (r * (w . 2)) by A4, A3, RVSUM_1:11;
reconsider rv9 = (1 - r) * v9, rw9 = r * w9 as Element of (TOP-REAL 3) ;
u9 = ((1 - r) * v9) + (r * w9)

proof

u9 = |[(((1 - r) * (v . 1)) + (r * (w . 1))),(((1 - r) * (v . 2)) + (r * (w . 2))),(((1 - r) * 1) + (r * 1))]| by A5, A3, A4, RVSUM_1:11
.= |[((1 - r) * (v . 1)),((1 - r) * (v . 2)),((1 - r) * 1)]| + |[(r * (w . 1)),(r * (w . 2)),(r * 1)]| by EUCLID_5:6
.= ((1 - r) * |[(v . 1),(v . 2),1]|) + |[(r * (w . 1)),(r * (w . 2)),(r * 1)]| by EUCLID_5:8
.= ((1 - r) * |[(v `1),(v `2),1]|) + (r * |[(w `1),(w `2),1]|) by EUCLID_5:8 ;
hence u9 = ((1 - r) * v9) + (r * w9) ; :: thesis: verum

end;

then u9 in { (((1 - r) * v9) + (r * w9)) where r is Real : ( 0 <= r & r <= 1 ) } by A1, A2;
hence |[(u `1),(u `2),1]| in LSeg (|[(v `1),(v `2),1]|,|[(w `1),(w `2),1]|) by RLTOPSP1:def 2; :: thesis: verum