let AFV be WeakAffVect; 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; ( 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
; 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; verum