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