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