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

A1: now :: thesis: ( ( a = p or MDist a,p ) implies PSym (p,a) = a )

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

end;

now :: thesis: ( not PSym (p,a) = a or a = p or MDist a,p )

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 ) ; :: thesis: verum

end;

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