let AFV be WeakAffVect; for a, b, c, p, p9, q, q9 being Element of AFV st a,b '||' p,p9 & a,c '||' q,q9 & a,p '||' p,b & a,q '||' q,c & a,p9 '||' p9,b & a,q9 '||' q9,c holds
ex r, r9 being Element of AFV st
( b,c '||' r,r9 & b,r '||' r,c & b,r9 '||' r9,c )
let a, b, c, p, p9, q, q9 be Element of AFV; ( a,b '||' p,p9 & a,c '||' q,q9 & a,p '||' p,b & a,q '||' q,c & a,p9 '||' p9,b & a,q9 '||' q9,c implies ex r, r9 being Element of AFV st
( b,c '||' r,r9 & b,r '||' r,c & b,r9 '||' r9,c ) )
assume
( a,b '||' p,p9 & a,c '||' q,q9 & a,p '||' p,b & a,q '||' q,c & a,p9 '||' p9,b & a,q9 '||' q9,c )
; ex r, r9 being Element of AFV st
( b,c '||' r,r9 & b,r '||' r,c & b,r9 '||' r9,c )
then
( a,b // b,a & a,c // c,a )
by Lm2;
then
b,c // c,b
by AFVECT0:12;
hence
ex r, r9 being Element of AFV st
( b,c '||' r,r9 & b,r '||' r,c & b,r9 '||' r9,c )
by Lm2; verum