let a, b, c, p, q, r be Point 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 )
assume that
A1:
a <> b
and
A2:
[a,b,p] in the Collinearity of CLS
and
A3:
[a,b,q] in the Collinearity of CLS
and
A4:
[a,b,r] in the Collinearity of CLS
; [p,q,r] in the Collinearity of CLS
A5:
( a = q or b = q )
by A1, A3, Lm5;
A6:
( a = r or b = r )
by A1, A4, Lm5;
A7:
( p in Z & q in Z )
;
A8:
r in Z
;
( a = p or b = p )
by A1, A2, Lm5;
hence
[p,q,r] in the Collinearity of CLS
by A5, A6, A7, A8; verum