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 :: thesis: ( MDist a,b implies MDist PSym (p,a), PSym (p,b) )

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 Th33;
PSym (p,a) <> PSym (p,b) by A2, Th30;
hence MDist PSym (p,a), PSym (p,b) by A3, Def2; :: thesis: verum

end;

now :: thesis: ( MDist PSym (p,a), PSym (p,b) implies MDist a,b )

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 Th33;
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