let AFV be WeakAffVect; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum