let AFV be WeakAffVect; for a, b, c, d, a9, b9, d9 being Element of AFV st a,b // a9,b9 & c,d // b,a & c,d9 // b9,a9 holds
d = d9
let a, b, c, d, a9, b9, d9 be Element of AFV; ( a,b // a9,b9 & c,d // b,a & c,d9 // b9,a9 implies d = d9 )
assume that
A1:
a,b // a9,b9
and
A2:
c,d // b,a
and
A3:
c,d9 // b9,a9
; d = d9
a9,b9 // a,b
by A1, Th3;
then
b9,a9 // b,a
by Th7;
then
c,d // b9,a9
by A2, Def1;
then
c,d // c,d9
by A3, Def1;
hence
d = d9
by Th4; verum