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