:: deftheorem defines parallelogram SEMI_AF1:def 3 :
for SAS being Semi_Affine_Space
for a, b, c, d being Element of SAS holds
( parallelogram a,b,c,d iff ( not a,b,c are_collinear & a,b // c,d & a,c // b,d ) );