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