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 on P & b on P & c on P ) )