let a, b, c, p, q, r be Point of CLS; :: thesis: ( a <> b & [a,b,p] in the Collinearity of CLS & [a,b,q] in the Collinearity of CLS & [a,b,r] in the Collinearity of CLS implies [p,q,r] in the Collinearity of CLS )
assume A1: ( a <> b & [a,b,p] in the Collinearity of CLS & [a,b,q] in the Collinearity of CLS & [a,b,r] in the Collinearity of CLS ) ; :: thesis: [p,q,r] in the Collinearity of CLS
thus [p,q,r] in the Collinearity of CLS :: thesis: verum

proof

( ( a = p or b = p ) & ( a = q or b = q ) & ( a = r or b = r ) & p in Z & q in Z & r in Z ) by A1, Lm5;
hence [p,q,r] in the Collinearity of CLS ; :: thesis: verum

end;