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 is_collinear
take b ; :: thesis: not for c being Point of CLS holds a,b,c is_collinear
take c ; :: thesis: not a,b,c is_collinear
not [a,b,c] in the Collinearity of CLS by Lm5;
hence not a,b,c is_collinear by Def2; :: thesis: verum