for OAS being OAffinSpace
for a, b, c, d, x being Element of OAS st Mid a,b,d & Mid a,x,c & not a,b,c are_collinear holds
ex y being Element of OAS st
( Mid b,y,c & Mid x,y,d )