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 that
A1: a <> c and
A2: b <> b' and
A3: a,b '||' b,c and
A4: 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' )
a,b' // b',c by A1, A4, Lm1;
then A5: Mid a,b',c by AFVECT0:def 3;
a,b // b,c by A1, A3, Lm1;
then Mid a,b,c by AFVECT0:def 3;
then MDist b,b' by A2, A5, AFVECT0:25;
then b,b' // b',b by AFVECT0:def 2;
then consider p, p' being Element of AFV such that
A6: b,b' '||' p,p' and
A7: ( 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 A6, A7;
hence ex p, p' being Element of AFV st
( p <> p' & b,b' '||' p,p' & b,p '||' p,b' & b,p' '||' p',b' ) by A2, A6, Lm5; :: thesis: verum