:: deftheorem defines are_collinear PENCIL_1:def 1 :
for S being TopStruct
for x, y being Point of S holds
( x,y are_collinear iff ( x = y or ex l being Block of S st {x,y} c= l ) );