let AFV be WeakAffVect; :: thesis: for a, b being Element of AFV holds a,a // b,b
let a, b be Element of AFV; :: thesis: a,a // b,b
consider p being Element of AFV such that
A1: a,a // b,p by Def1;
b,p // a,a by A1, Th4;
hence a,a // b,b by A1, Def1; :: thesis: verum