let S be non empty satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c, d being POINT of S st a <> b & Collinear a,b,c & Collinear a,b,d holds
Collinear a,c,d
let a, b, c, d be POINT of S; :: thesis: ( a <> b & Collinear a,b,c & Collinear a,b,d implies Collinear a,c,d )
assume that
A1: a <> b and
A2: Collinear a,b,c and
A3: Collinear a,b,d ; :: thesis: Collinear a,c,d

per cases ( a = c or a <> c ) ;

suppose a = c ; :: thesis: Collinear a,c,d

hence Collinear a,c,d by Prelim05; :: thesis: verum

end;

suppose a <> c ; :: thesis: Collinear a,c,d

then A4: Line (a,b) = Line (a,c) by A1, A2, Prelim07;
d in { y where y is POINT of S : Collinear a,b,y } by A3;
then d in Line (a,c) by A4, GTARSKI3:def 10;
then Collinear d,a,c by LemmaA2;
hence Collinear a,c,d by GTARSKI3:45; :: thesis: verum

end;

end;