let AFV be WeakAffVect; :: thesis: for a, b, c, d being Element of AFV st a,b '||' c,d holds
b,a '||' c,d
let a, b, c, d be Element of AFV; :: thesis: ( a,b '||' c,d implies b,a '||' c,d )
assume a,b '||' c,d ; :: thesis: b,a '||' c,d
then ( a,b // c,d or a,b // d,c ) by DIRAF:def 4;
then ( b,a // d,c or b,a // c,d ) by AFVECT0:7;
hence b,a '||' c,d by DIRAF:def 4; :: thesis: verum