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: 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 A2, Th25; :: thesis: verum

end;

now

assume A3: 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 A3, Th29; :: thesis: verum

end;

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