let A, B, C, D be Point of (TOP-REAL 2); ( B in LSeg (A,C) & D in LSeg (A,B) implies B in LSeg (D,C) )
assume that
A1:
B in LSeg (A,C)
and
A2:
D in LSeg (A,B)
; B in LSeg (D,C)
A3:
(dist (A,D)) + (dist (D,C)) = dist (A,C)
by A1, A2, THORANGE, EUCLID12:12;
A4:
(dist (A,B)) + (dist (B,C)) = dist (A,C)
by A1, EUCLID12:12;
(dist (A,D)) + (dist (D,B)) = dist (A,B)
by A2, EUCLID12:12;
then
(dist (D,B)) + (dist (B,C)) = dist (D,C)
by A3, A4;
hence
B in LSeg (D,C)
by EUCLID12:12; verum