let AFV be WeakAffVect; :: thesis: for a, b being Element of holds a,a // b,b
let a, b be Element of ; :: thesis: a,a // b,b
consider p being Element of 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