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 MDist a,b ; :: thesis: MDist PSym p,a, PSym p,b
then ( a,b // b,a & a <> b ) by Def2;
then ( PSym p,a, PSym p,b // PSym p,b, PSym p,a & PSym p,a <> PSym p,b ) by Th37, Th40;
hence MDist PSym p,a, PSym p,b by Def2; :: thesis: verum

end;

now

assume MDist PSym p,a, PSym p,b ; :: thesis: MDist a,b
then ( PSym p,a, PSym p,b // PSym p,b, PSym p,a & PSym p,a <> PSym p,b ) by Def2;
then ( a,b // b,a & a <> b ) by Th40;
hence MDist a,b by Def2; :: thesis: verum

end;

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