for OAS being OAffinSpace
for a, b, c being Element of OAS
for a9, b9, c9 being Element of (Lambda OAS) st a = a9 & b = b9 & c = c9 holds
( a,b,c are_collinear iff LIN a9,b9,c9 )