for AFV being WeakAffVect
for a, b, c, d, p being Element of AFV holds
( a,b // c,d iff PSym (p,a), PSym (p,b) // PSym (p,c), PSym (p,d) )