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