:: deftheorem defines are_collinear COLLSP:def 2 :
for CS being non empty CollStr
for a, b, c being Point of CS holds
( a,b,c are_collinear iff [a,b,c] in the Collinearity of CS );