let AFV be WeakAffVect; :: thesis: for a, b, c being Element of AFV st a,b '||' b,c & a <> c holds
a,b // b,c
let a, b, c be Element of AFV; :: thesis: ( a,b '||' b,c & a <> c implies a,b // b,c )
assume that
A1: a,b '||' b,c and
A2: a <> c ; :: thesis: a,b // b,c
not a,b // c,b by A2, AFVECT0:4, AFVECT0:7;
hence a,b // b,c by A1, DIRAF:def 4; :: thesis: verum