let AFV be WeakAffVect; :: thesis: for a, b, c, d, p, q being Element of AFV st a,b '||' p,q & c,d '||' p,q holds
a,b '||' c,d
let a, b, c, d, p, q be Element of AFV; :: thesis: ( a,b '||' p,q & c,d '||' p,q implies a,b '||' c,d )
assume ( a,b '||' p,q & c,d '||' p,q ) ; :: thesis: a,b '||' c,d
then ( ( a,b // p,q & c,d // p,q ) or ( a,b // p,q & c,d // q,p ) or ( a,b // q,p & c,d // p,q ) or ( a,b // q,p & c,d // q,p ) ) by DIRAF:def 4;
then ( a,b // c,d or ( a,b // p,q & d,c // p,q ) or ( a,b // q,p & d,c // q,p ) ) by AFVECT0:7, AFVECT0:def 1;
then ( a,b // c,d or a,b // d,c ) by AFVECT0:def 1;
hence a,b '||' c,d by DIRAF:def 4; :: thesis: verum