:: deftheorem defines are_collinear PROJPL_1:def 5 :
for G being IncProjStr
for a, b, c being POINT of G holds
( a,b,c are_collinear iff ex P being LINE of G st {a,b,c} on P );