let AFV be WeakAffVect; :: thesis: for a, b, c, d, b' being Element of AFV st a,b // c,d & a,c // b',d holds
b = b'
let a, b, c, d, b' be Element of AFV; :: thesis: ( a,b // c,d & a,c // b',d implies b = b' )
assume A1: ( a,b // c,d & a,c // b',d ) ; :: thesis: b = b'
then a,c // b,d by Def1;
then b,d // a,c by Th4;
then A2: d,b // c,a by Th8;
b',d // a,c by A1, Th4;
then d,b' // c,a by Th8;
then d,b // d,b' by A2, Def1;
hence b = b' by Th5; :: thesis: verum