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