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