let AFV be WeakAffVect; :: thesis: for a, b, b9, c being Element of AFV st a <> c & b <> b9 & a,b '||' b,c & a,b9 '||' b9,c holds
ex p, p9 being Element of AFV st
( p <> p9 & b,b9 '||' p,p9 & b,p '||' p,b9 & b,p9 '||' p9,b9 )
let a, b, b9, c be Element of AFV; :: thesis: ( a <> c & b <> b9 & a,b '||' b,c & a,b9 '||' b9,c implies ex p, p9 being Element of AFV st
( p <> p9 & b,b9 '||' p,p9 & b,p '||' p,b9 & b,p9 '||' p9,b9 ) )
assume that
A1: a <> c and
A2: b <> b9 and
A3: a,b '||' b,c and
A4: a,b9 '||' b9,c ; :: thesis: ex p, p9 being Element of AFV st
( p <> p9 & b,b9 '||' p,p9 & b,p '||' p,b9 & b,p9 '||' p9,b9 )
a,b9 // b9,c by A1, A4, Lm1;
then A5: Mid a,b9,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,b9 by A2, A5, AFVECT0:20;
then b,b9 // b9,b by AFVECT0:def 2;
then consider p, p9 being Element of AFV such that
A6: b,b9 '||' p,p9 and
A7: ( b,p '||' p,b9 & b,p9 '||' p9,b9 ) by Lm2;
( p <> p9 implies ex p, p9 being Element of AFV st
( p <> p9 & b,b9 '||' p,p9 & b,p '||' p,b9 & b,p9 '||' p9,b9 ) ) by A6, A7;
hence ex p, p9 being Element of AFV st
( p <> p9 & b,b9 '||' p,p9 & b,p '||' p,b9 & b,p9 '||' p9,b9 ) by A2, A6, Lm5; :: thesis: verum