let AFV be WeakAffVect; :: thesis: for a, a', b, b', p being Element of AFV st a <> a' & b <> b' & p,a '||' p,a' & p,b '||' p,b' holds
a,b '||' a',b'
let a, a', b, b', p be Element of AFV; :: thesis: ( a <> a' & b <> b' & p,a '||' p,a' & p,b '||' p,b' implies a,b '||' a',b' )
assume ( a <> a' & b <> b' & p,a '||' p,a' & p,b '||' p,b' ) ; :: thesis: a,b '||' a',b'
then ( a,p // p,a' & b,p // p,b' ) by Lm1, Lm3;
then ( Mid a,p,a' & Mid b,p,b' ) by AFVECT0:def 3;
then a,b // b',a' by AFVECT0:30;
hence a,b '||' a',b' by DIRAF:def 4; :: thesis: verum