for a, b, c, p, q, r being Point of CLS holds
( ( ( a = b or a = c or b = c ) implies [a,b,c] in the Collinearity of CLS ) & ( 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 ) ) by Lm5, Lm6;
hence CLS is CollSp by Def3, Def4; :: thesis: verum