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

A1: now

assume A2: MDist a,b ; :: thesis: MDist PSym p,a, PSym p,b
then a,b // b,a by Def2;
then A3: PSym p,a, PSym p,b // PSym p,b, PSym p,a by Th40;
PSym p,a <> PSym p,b by A2, Th37;
hence MDist PSym p,a, PSym p,b by A3, Def2; :: thesis: verum

end;

now

assume A4: MDist PSym p,a, PSym p,b ; :: thesis: MDist a,b
then PSym p,a, PSym p,b // PSym p,b, PSym p,a by Def2;
then a,b // b,a by Th40;
hence MDist a,b by A4, Def2; :: thesis: verum

end;

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