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