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

now

assume A2: z <> x ; :: thesis: x,y,t is_collinear
x,y '||' x,z by A1, Def5;
then x,z '||' z,t by A1, Th28;
then z,x '||' z,t by Th27;
then z,x,t is_collinear by Def5;
then ( x,z,t is_collinear & x,z,y is_collinear & x,z,x is_collinear ) by A1, Th36, Th37;
hence x,y,t is_collinear by A2, Th38; :: thesis: verum

end;

hence x,y,t is_collinear by A1, Def5; :: thesis: verum