for AFV being WeakAffVect
for a, b, c, p being Element of AFV holds
( Mid a,b,c iff Mid PSym (p,a), PSym (p,b), PSym (p,c) ) by Th33;