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 that
A1: x <> y and
A2: x,y,z is_collinear and
A3: x,y,t is_collinear and
A4: x,y,u is_collinear ; :: thesis: z,t,u is_collinear

A5: now

A6: x,y '||' x,z by A2, Def5;
x,y '||' x,u by A4, Def5;
then x,z '||' x,u by A1, A6, Th28;
then A7: z,x '||' z,u by Th26;
x,y '||' x,t by A3, Def5;
then x,z '||' x,t by A1, A6, Th28;
then A8: z,x '||' z,t by Th26;
assume x <> z ; :: thesis: z,t,u is_collinear
then z,t '||' z,u by A8, A7, Th28;
hence z,t,u is_collinear by Def5; :: thesis: verum

end;

now

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

end;

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