let AFV be WeakAffVect; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: verum