:: deftheorem defines Line COLLSP:def 5 :
for CLSP being CollSp
for a, b being Point of CLSP holds Line (a,b) = { p where p is Point of CLSP : a,b,p are_collinear } ;