let AFV be WeakAffVect; for a, b, c, b9 being Element of AFV st Mid a,b,c & Mid a,b9,c & not b = b9 holds
MDist b,b9
let a, b, c, b9 be Element of AFV; ( Mid a,b,c & Mid a,b9,c & not b = b9 implies MDist b,b9 )
assume that
A1:
Mid a,b,c
and
A2:
Mid a,b9,c
; ( b = b9 or MDist b,b9 )
A3:
a,b // b,c
by A1;
consider d being Element of AFV such that
A4:
b9,c // b,d
by Def1;
A5:
b,d // b9,c
by A4, Th3;
then
b,b9 // d,c
by Def1;
then A6:
b9,b // c,d
by Th7;
a,b9 // b9,c
by A2;
then
a,b9 // b,d
by A5, Def1;
then
b,b9 // c,d
by A3, Def1;
then
b,b9 // b9,b
by A6, Def1;
hence
( b = b9 or MDist b,b9 )
; verum