reconsider a = 1, b = 2, c = 3 as Point of CLS by ENUMSET1:def 1;
take a ; :: thesis: not for b, c being Point of CLS holds a,b,c are_collinear
take b ; :: thesis: not for c being Point of CLS holds a,b,c are_collinear
take c ; :: thesis: not a,b,c are_collinear
not [a,b,c] in the Collinearity of CLS by Lm5;
hence not a,b,c are_collinear ; :: thesis: verum