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 that
A1: a <> a' and
A2: b <> b' and
A3: p,a '||' p,a' and
A4: p,b '||' p,b' ; :: thesis: a,b '||' a',b'
b,p // p,b' by A2, A4, Lm1, Lm3;
then A5: Mid b,p,b' by AFVECT0:def 3;
a,p // p,a' by A1, A3, Lm1, Lm3;
then Mid a,p,a' by AFVECT0:def 3;
then a,b // b',a' by A5, AFVECT0:30;
hence a,b '||' a',b' by DIRAF:def 4; :: thesis: verum