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

A1: now

assume A2: MDist p,q ; :: thesis: PSym (p,a) = PSym (q,a)
( Mid a,p, PSym (p,a) & Mid a,q, PSym (q,a) ) by Def4;
hence PSym (p,a) = PSym (q,a) by A2, Th29; :: thesis: verum

end;

now

assume A3: PSym (p,a) = PSym (q,a) ; :: thesis: ( p = q or MDist p,q )
( Mid a,p, PSym (p,a) & Mid a,q, PSym (q,a) ) by Def4;
hence ( p = q or MDist p,q ) by A3, Th25; :: thesis: verum

end;

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