let AFV be WeakAffVect; :: thesis: for a, b, b', c being Element of AFV st a <> c & b <> b' & a,b '||' b,c & a,b' '||' b',c holds
ex p, p' being Element of AFV st
( p <> p' & b,b' '||' p,p' & b,p '||' p,b' & b,p' '||' p',b' )
let a, b, b', c be Element of AFV; :: thesis: ( a <> c & b <> b' & a,b '||' b,c & a,b' '||' b',c implies ex p, p' being Element of AFV st
( p <> p' & b,b' '||' p,p' & b,p '||' p,b' & b,p' '||' p',b' ) )
assume A1: ( a <> c & b <> b' & a,b '||' b,c & a,b' '||' b',c ) ; :: thesis: ex p, p' being Element of AFV st
( p <> p' & b,b' '||' p,p' & b,p '||' p,b' & b,p' '||' p',b' )
then ( b <> b' & a,b // b,c & a,b' // b',c ) by Lm1;
then ( b <> b' & Mid a,b,c & Mid a,b',c ) by AFVECT0:def 3;
then ( b <> b' & MDist b,b' ) by AFVECT0:25;
then b,b' // b',b by AFVECT0:def 2;
then consider p, p' being Element of AFV such that
A2: ( b,b' '||' p,p' & b,p '||' p,b' & b,p' '||' p',b' ) by Lm2;
( p <> p' implies ex p, p' being Element of AFV st
( p <> p' & b,b' '||' p,p' & b,p '||' p,b' & b,p' '||' p',b' ) ) by A2;
hence ex p, p' being Element of AFV st
( p <> p' & b,b' '||' p,p' & b,p '||' p,b' & b,p' '||' p',b' ) by A1, A2, Lm5; :: thesis: verum