for SAS being Semi_Affine_Space
for a, b, c, d, x being Element of SAS holds
( not parallelogram a,b,c,d or not a,b,x are_collinear or not c,d,x are_collinear )