let AFV be WeakAffVect; 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; 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
; a,b '||' b,c
thus
a,b '||' b,c
by A1, DIRAF:def 4; verum