:: deftheorem Def4 defines PSym AFVECT0:def 4 :
for AFV being WeakAffVect
for a, b, b₄ being Element of AFV holds
( b₄ = PSym (a,b) iff Mid b,a,b₄ );