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

let a, c be Element of AFV; :: thesis: ex b being Element of AFV st a,b '||' b,c

consider b being Element of AFV such that

A1: a,b // b,c by AFVECT0:def 1;

take b ; :: thesis: a,b '||' b,c

thus a,b '||' b,c by A1, DIRAF:def 4; :: thesis: verum

let a, c be Element of AFV; :: thesis: ex b being Element of AFV st a,b '||' b,c

consider b being Element of AFV such that

A1: a,b // b,c by AFVECT0:def 1;

take b ; :: thesis: a,b '||' b,c

thus a,b '||' b,c by A1, DIRAF:def 4; :: thesis: verum