let AFV be WeakAffVect; :: thesis: for a, b, c being Element of AFV st a,b // a,c holds
b = c
let a, b, c be Element of AFV; :: thesis: ( a,b // a,c implies b = c )
assume a,b // a,c ; :: thesis: b = c
then a,a // b,c by Def1;
then b,c // a,a by Th3;
hence b = c by Def1; :: thesis: verum