hereby :: thesis: ( ( for p, q, r, r1, r2 being Element of CS st p <> q & p,q,r is_collinear & p,q,r1 is_collinear & p,q,r2 is_collinear holds
r,r1,r2 is_collinear ) implies CS is transitive )

assume A4: CS is transitive ; :: thesis: for p, q, r, r1, r2 being Element of CS st p <> q & p,q,r is_collinear & p,q,r1 is_collinear & p,q,r2 is_collinear holds
r,r1,r2 is_collinear
let p, q, r, r1, r2 be Element of CS; :: thesis: ( p <> q & p,q,r is_collinear & p,q,r1 is_collinear & p,q,r2 is_collinear implies r,r1,r2 is_collinear )
assume that
A5: p <> q and
A6: ( p,q,r is_collinear & p,q,r1 is_collinear ) and
A7: p,q,r2 is_collinear ; :: thesis: r,r1,r2 is_collinear
A8: [p,q,r2] in the Collinearity of CS by A7, COLLSP:def 2;
( [p,q,r] in the Collinearity of CS & [p,q,r1] in the Collinearity of CS ) by A6, COLLSP:def 2;
then [r,r1,r2] in the Collinearity of CS by A4, A5, A8, COLLSP:def 4;
hence r,r1,r2 is_collinear by COLLSP:def 2; :: thesis: verum

end;

assume A9: for p, q, r, r1, r2 being Element of CS st p <> q & p,q,r is_collinear & p,q,r1 is_collinear & p,q,r2 is_collinear holds
r,r1,r2 is_collinear ; :: thesis: CS is transitive
let p, q, r, r1, r2 be Element of CS; :: according to COLLSP:def 4 :: thesis: ( p = q or not [p,q,r] in the Collinearity of CS or not [p,q,r1] in the Collinearity of CS or not [p,q,r2] in the Collinearity of CS or [r,r1,r2] in the Collinearity of CS )
assume that
A10: p <> q and
A11: ( [p,q,r] in the Collinearity of CS & [p,q,r1] in the Collinearity of CS ) and
A12: [p,q,r2] in the Collinearity of CS ; :: thesis: [r,r1,r2] in the Collinearity of CS
A13: p,q,r2 is_collinear by A12, COLLSP:def 2;
( p,q,r is_collinear & p,q,r1 is_collinear ) by A11, COLLSP:def 2;
then r,r1,r2 is_collinear by A9, A10, A13;
hence [r,r1,r2] in the Collinearity of CS by COLLSP:def 2; :: thesis: verum