thus
( CS is transitive implies for p, q, r, r1, r2 being Element of CS st p <> q & p,q,r are_collinear & p,q,r1 are_collinear & p,q,r2 are_collinear holds

r,r1,r2 are_collinear ) ; :: thesis: ( ( for p, q, r, r1, r2 being Element of CS st p <> q & p,q,r are_collinear & p,q,r1 are_collinear & p,q,r2 are_collinear holds

r,r1,r2 are_collinear ) implies CS is transitive )

assume A3: for p, q, r, r1, r2 being Element of CS st p <> q & p,q,r are_collinear & p,q,r1 are_collinear & p,q,r2 are_collinear holds

r,r1,r2 are_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

A4: p <> q and

A5: ( [p,q,r] in the Collinearity of CS & [p,q,r1] in the Collinearity of CS ) and

A6: [p,q,r2] in the Collinearity of CS ; :: thesis: [r,r1,r2] in the Collinearity of CS

A7: p,q,r2 are_collinear by A6;

( p,q,r are_collinear & p,q,r1 are_collinear ) by A5;

then r,r1,r2 are_collinear by A3, A4, A7;

hence [r,r1,r2] in the Collinearity of CS ; :: thesis: verum

r,r1,r2 are_collinear ) ; :: thesis: ( ( for p, q, r, r1, r2 being Element of CS st p <> q & p,q,r are_collinear & p,q,r1 are_collinear & p,q,r2 are_collinear holds

r,r1,r2 are_collinear ) implies CS is transitive )

assume A3: for p, q, r, r1, r2 being Element of CS st p <> q & p,q,r are_collinear & p,q,r1 are_collinear & p,q,r2 are_collinear holds

r,r1,r2 are_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

A4: p <> q and

A5: ( [p,q,r] in the Collinearity of CS & [p,q,r1] in the Collinearity of CS ) and

A6: [p,q,r2] in the Collinearity of CS ; :: thesis: [r,r1,r2] in the Collinearity of CS

A7: p,q,r2 are_collinear by A6;

( p,q,r are_collinear & p,q,r1 are_collinear ) by A5;

then r,r1,r2 are_collinear by A3, A4, A7;

hence [r,r1,r2] in the Collinearity of CS ; :: thesis: verum