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

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

x,y '||' x,z by A2;
then x,z '||' z,t by A1, A3, Th23;
then z,x '||' z,t by Th22;
then z,x,t are_collinear ;
then A4: x,z,t are_collinear by Th30;
assume A5: z <> x ; :: thesis: x,y,t are_collinear
( x,z,y are_collinear & x,z,x are_collinear ) by A2, Th30, Th31;
hence x,y,t are_collinear by A5, A4, Th32; :: thesis: verum

end;

hence x,y,t are_collinear by A3; :: thesis: verum