let S be OAffinSpace; :: thesis: for x, y, z, t, u being Element of S st x <> y & x,y,z are_collinear & x,y,t are_collinear & x,y,u are_collinear holds
z,t,u are_collinear
let x, y, z, t, u be Element of S; :: thesis: ( x <> y & x,y,z are_collinear & x,y,t are_collinear & x,y,u are_collinear implies z,t,u are_collinear )
assume that
A1: x <> y and
A2: x,y,z are_collinear and
A3: x,y,t are_collinear and
A4: x,y,u are_collinear ; :: thesis: z,t,u are_collinear

A5: now :: thesis: ( x <> z implies z,t,u are_collinear )

A6: x,y '||' x,z by A2;
x,y '||' x,u by A4;
then x,z '||' x,u by A1, A6, Th23;
then A7: z,x '||' z,u by Th21;
x,y '||' x,t by A3;
then x,z '||' x,t by A1, A6, Th23;
then A8: z,x '||' z,t by Th21;
assume x <> z ; :: thesis: z,t,u are_collinear
then z,t '||' z,u by A8, A7, Th23;
hence z,t,u are_collinear ; :: thesis: verum

end;

( x = z implies z,t,u are_collinear ) by A3, A4, A1, Th23;
hence z,t,u are_collinear by A5; :: thesis: verum