let AFV be WeakAffVect; :: thesis: for p, a, b being Element of AFV holds
( PSym (p,a) = b iff a,p // p,b )
let p, a, b be Element of AFV; :: thesis: ( PSym (p,a) = b iff a,p // p,b )

A1: now

assume a,p // p,b ; :: thesis: PSym (p,a) = b
then Mid a,p,b by Def3;
hence PSym (p,a) = b by Def4; :: thesis: verum

end;

now

assume PSym (p,a) = b ; :: thesis: a,p // p,b
then Mid a,p,b by Def4;
hence a,p // p,b by Def3; :: thesis: verum

end;

hence ( PSym (p,a) = b iff a,p // p,b ) by A1; :: thesis: verum