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