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