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

now :: thesis: ( x <> y implies x,y,w are_collinear )

assume A4: x <> y ; :: thesis: x,y,w are_collinear
x,y,x are_collinear by Th31;
then A5: z,u,x are_collinear by A2, A4, Th32;
x,y,y are_collinear by Th31;
then A6: z,u,y are_collinear by A2, A4, Th32;
z,u,w are_collinear by A3, Th30;
hence x,y,w are_collinear by A1, A6, A5, Th32; :: thesis: verum

end;

hence x,y,w are_collinear by Th31; :: thesis: verum