:: deftheorem defines congr SEMI_AF1:def 4 :
for SAS being Semi_Affine_Space
for a, b, r, s being Element of SAS holds
( congr a,b,r,s iff ( ( a = b & r = s ) or ex p, q being Element of SAS st
( parallelogram p,q,a,b & parallelogram p,q,r,s ) ) );