let AFV be WeakAffVect; :: thesis: for a, b, c, d, p being Element of AFV holds
( a,b // c,d iff PSym p,a, PSym p,b // PSym p,c, PSym p,d )
let a, b, c, d, p be Element of AFV; :: thesis: ( a,b // c,d iff PSym p,a, PSym p,b // PSym p,c, PSym p,d )

A1: now

assume A2: PSym p,a, PSym p,b // PSym p,c, PSym p,d ; :: thesis: a,b // c,d
d,c // PSym p,c, PSym p,d by Th39;
then d,c // PSym p,a, PSym p,b by A2, Def1;
then A3: c,d // PSym p,b, PSym p,a by Th8;
a,b // PSym p,b, PSym p,a by Th39;
hence a,b // c,d by A3, Def1; :: thesis: verum

end;

now

A4: PSym p,b, PSym p,a // a,b by Th4, Th39;
assume A5: a,b // c,d ; :: thesis: PSym p,a, PSym p,b // PSym p,c, PSym p,d
PSym p,d, PSym p,c // c,d by Th4, Th39;
then PSym p,d, PSym p,c // a,b by A5, Def1;
then PSym p,b, PSym p,a // PSym p,d, PSym p,c by A4, Def1;
hence PSym p,a, PSym p,b // PSym p,c, PSym p,d by Th8; :: thesis: verum

end;

hence ( a,b // c,d iff PSym p,a, PSym p,b // PSym p,c, PSym p,d ) by A1; :: thesis: verum