let A, B, C, D be Element of (TOP-REAL 2); ( B <> C & B in LSeg (A,C) & C in LSeg (B,D) implies C in LSeg (A,D) )
assume that
A1:
B <> C
and
A2:
B in LSeg (A,C)
and
A3:
C in LSeg (B,D)
; C in LSeg (A,D)
reconsider OAS = OASpace (TOP-REAL 2) as OAffinSpace by THQQ;
reconsider ta = A, tb = B, tc = C, td = D as Element of OAS ;
( Mid ta,tb,tc & Mid tb,tc,td )
by A2, A3, THSS2;
then
ex u, v being Point of (TOP-REAL 2) st
( u = ta & v = td & tc in LSeg (u,v) )
by A1, DIRAF:12, THSS2;
hence
C in LSeg (A,D)
; verum