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

A1: now

assume PSym (p,(PSym (q,a))) = PSym (q,(PSym (p,a))) ; :: thesis: ( ( p = q or MDist q,p or MDist q, PSym (p,q) ) & ( p = q or MDist p,q or MDist q, PSym (p,q) ) )
then PSym (p,(PSym (q,(PSym (p,a))))) = PSym (q,a) by Th36;
then PSym ((PSym (p,q)),a) = PSym (q,a) by Th44;
then ( q = PSym (p,q) or MDist q, PSym (p,q) ) by Th43;
then A2: ( Mid q,p,q or MDist q, PSym (p,q) ) by Def4;
hence ( p = q or MDist q,p or MDist q, PSym (p,q) ) by Th23; :: thesis: ( p = q or MDist p,q or MDist q, PSym (p,q) )
thus ( p = q or MDist p,q or MDist q, PSym (p,q) ) by A2, Th23; :: thesis: verum

end;

now

assume ( p = q or MDist p,q or MDist q, PSym (p,q) ) ; :: thesis: PSym (p,(PSym (q,a))) = PSym (q,(PSym (p,a)))
then ( Mid q,p,q or MDist q, PSym (p,q) ) by Th23;
then PSym ((PSym (p,q)),a) = PSym (q,a) by Def4, Th43;
then PSym (p,(PSym (q,(PSym (p,a))))) = PSym (q,a) by Th44;
hence PSym (p,(PSym (q,a))) = PSym (q,(PSym (p,a))) by Th36; :: thesis: verum

end;

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