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