let AFV be WeakAffVect; :: thesis: for a, p, q 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 a, p, q 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 :: thesis: ( PSym (p,(PSym (q,a))) = PSym (q,(PSym (p,a))) implies ( ( p = q or MDist q,p or MDist q, PSym (p,q) ) & ( p = q or MDist p,q or MDist q, PSym (p,q) ) ) )

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 Th29;
then PSym ((PSym (p,q)),a) = PSym (q,a) by Th37;
then ( q = PSym (p,q) or MDist q, PSym (p,q) ) by Th36;
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) ) ; :: 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, Th18; :: thesis: verum

end;

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

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 Th18;
then PSym ((PSym (p,q)),a) = PSym (q,a) by Def4, Th36;
then PSym (p,(PSym (q,(PSym (p,a))))) = PSym (q,a) by Th37;
hence PSym (p,(PSym (q,a))) = PSym (q,(PSym (p,a))) by Th29; :: 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