let A, B, C, D be Point of (TOP-REAL 2); :: thesis: ( 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) ; :: thesis: 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; :: thesis: verum