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

A1: now

assume ( a = p or MDist a,p ) ; :: thesis: PSym p,a = a
then Mid a,p,a by Th23;
hence PSym p,a = a by Def4; :: thesis: verum

end;

now

assume PSym p,a = a ; :: thesis: ( a = p or MDist a,p )
then Mid a,p,a by Def4;
hence ( a = p or MDist a,p ) by Th23; :: thesis: verum

end;

hence ( PSym p,a = a iff ( a = p or MDist a,p ) ) by A1; :: thesis: verum