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 that
A1: a,b '||' b,c and
A2: ( b,b' '||' p,p' & b,p '||' p,b' & b,p' '||' p',b' ) ; :: thesis: a,b' '||' b',c
A3: b,b' // b',b by A2, Lm2;

A4: now

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

A7: now

assume MDist b,b' ; :: thesis: a,b' '||' b',c
then Mid a,b',c by A6, 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 A5, DIRAF:def 4;
hence a,b' '||' b',c by A3, A7, 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, A4, DIRAF:def 4; :: thesis: verum