let AFV be WeakAffVect; :: thesis: for a, b, p being Element of AFV st a,b '||' p,p holds

a = b

let a, b, p be Element of AFV; :: thesis: ( a,b '||' p,p implies a = b )

assume a,b '||' p,p ; :: thesis: a = b

then a,b // p,p by DIRAF:def 4;

hence a = b by AFVECT0:def 1; :: thesis: verum

a = b

let a, b, p be Element of AFV; :: thesis: ( a,b '||' p,p implies a = b )

assume a,b '||' p,p ; :: thesis: a = b

then a,b // p,p by DIRAF:def 4;

hence a = b by AFVECT0:def 1; :: thesis: verum