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