for OAS being OAffinSpace
for a, a9, b, b9, c, c9 being Element of OAS st not a,b,a9 are_collinear & a,a9 '||' b,b9 & a,a9 '||' c,c9 & Mid a,b,c & a9,b9,c9 are_collinear holds
Mid a9,b9,c9