let AFV be WeakAffVect; :: thesis: for a, b, b', p, p', c being Element of AFV st a,b '||' b,c & b,b' '||' p,p' & b,p '||' p,b' & b,p' '||' p',b' holds
a,b' '||' b',c
let a, b, b', p, p', c be Element of AFV; :: thesis: ( a,b '||' b,c & b,b' '||' p,p' & b,p '||' p,b' & b,p' '||' p',b' implies a,b' '||' b',c )
assume A1: ( a,b '||' b,c & b,b' '||' p,p' & b,p '||' p,b' & b,p' '||' p',b' ) ; :: thesis: a,b' '||' b',c
then A2: ( a,b '||' b,c & b,b' // b',b ) by Lm2;

A3: now

assume A4: a,b // b,c ; :: thesis: a,b' '||' b',c
then A5: Mid a,b,c by AFVECT0:def 3;

A6: now

assume MDist b,b' ; :: thesis: a,b' '||' b',c
then Mid a,b',c by A5, AFVECT0:28;
then a,b' // b',c by AFVECT0:def 3;
hence a,b' '||' b',c by DIRAF:def 4; :: thesis: verum

end;

( b = b' implies a,b' '||' b',c ) by A4, DIRAF:def 4;
hence a,b' '||' b',c by A2, A6, AFVECT0:def 2; :: thesis: verum

end;

now

assume a,b // c,b ; :: thesis: a,b' '||' b',c
then a = c by AFVECT0:5, AFVECT0:8;
then a,b' // c,b' by AFVECT0:2;
hence a,b' '||' b',c by DIRAF:def 4; :: thesis: verum

end;

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