let AFV be WeakAffVect; :: thesis: for a, a9, b, b9, p being Element of AFV st a <> a9 & b <> b9 & p,a '||' p,a9 & p,b '||' p,b9 holds
a,b '||' a9,b9
let a, a9, b, b9, p be Element of AFV; :: thesis: ( a <> a9 & b <> b9 & p,a '||' p,a9 & p,b '||' p,b9 implies a,b '||' a9,b9 )
assume that
A1: a <> a9 and
A2: b <> b9 and
A3: p,a '||' p,a9 and
A4: p,b '||' p,b9 ; :: thesis: a,b '||' a9,b9
b,p // p,b9 by A2, A4, Lm1, Lm3;
then A5: Mid b,p,b9 by AFVECT0:def 3;
a,p // p,a9 by A1, A3, Lm1, Lm3;
then Mid a,p,a9 by AFVECT0:def 3;
then a,b // b9,a9 by A5, AFVECT0:25;
hence a,b '||' a9,b9 by DIRAF:def 4; :: thesis: verum