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

now

assume A4: x <> y ; :: thesis: x,y,w is_collinear
x,y,x is_collinear by Th37;
then A5: z,u,x is_collinear by A2, A4, Th38;
x,y,y is_collinear by Th37;
then A6: z,u,y is_collinear by A2, A4, Th38;
z,u,w is_collinear by A3, Th36;
hence x,y,w is_collinear by A1, A6, A5, Th38; :: thesis: verum

end;

hence x,y,w is_collinear by Th37; :: thesis: verum