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

A2: now

assume x = z ; :: thesis: z,t,u is_collinear
then ( z <> y & z,y '||' z,t & z,y '||' z,u ) by A1, Def5;
then z,t '||' z,u by Th28;
hence z,t,u is_collinear by Def5; :: thesis: verum

end;

now

assume A3: x <> z ; :: thesis: z,t,u is_collinear
( x,y '||' x,z & x,y '||' x,t & x,y '||' x,u ) by A1, Def5;
then ( x,z '||' x,t & x,z '||' x,u ) by A1, Th28;
then ( z,x '||' z,t & z,x '||' z,u ) by Th26;
then z,t '||' z,u by A3, Th28;
hence z,t,u is_collinear by Def5; :: thesis: verum

end;

hence z,t,u is_collinear by A2; :: thesis: verum