let AFV be WeakAffVect; :: thesis: for a, b being Element of holds a,b // a,b
let a, b be Element of ; :: thesis: a,b // a,b
ex d being Element of st a,b // b,d by Def1;
hence a,b // a,b by Def1; :: thesis: verum